CCS as a specification and verification technique: a case study and a comparison with temporal logic