University of Hertfordshire

By the same authors

A CCS case study: a safety-critical system

Research output: Book/ReportOther report

Documents

View graph of relations
Original languageEnglish
PublisherUniversity of Hertfordshire
Publication statusPublished - 1990

Publication series

NameUH Computer Science Technical Report
PublisherUniversity of Hertfordshire
Volume103

Abstract

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.

ID: 91508