A CCS case study: a safety-critical system

A level crossing control system is specified in CCS, motivated by a temporal logic specification of the safety requirements. We show 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. By applying the technique of bisimulation, it is proved that the crossing satisfies the full safety requirements.