A CCS cast study: a safety-critical system

A level-crossing control system is specified in the Calculus of Communicating Systems (R. Milner, 1980), motivated by a temporal logic specification of the safety requirements. The author shows that, with certain reservations, these can be satisfactorily stated entirely within CCS. The crossing system is divided into two smaller subsystems, which are shown to be equivalent to the original single system, and whose behaviour is then analysed using the methods of the calculus. She also shows that the crossing satisfies the safety requirements; there is no bisimulation although the system is both `may´ and `must´ equivalent to the specification. Some of the implications of this are discussed