A CCS case study: a safety-critical system
Jean Baillie · Software Engineering Journal · 1991
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. We also show 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.