Modelling a Safety-Critical System through CCS

摘要

Model checking is a technique for automatically verifying the correctness of properties of finite-state systems in computer science. This paper deals with the modeling of a safety critical system, named "A level-crossing control system". The specifications of the model are expressed as processes in the calculus of communicating systems (CCS). The requirements of the system are written in the form of properties or formula in temporal logic and Mu-calculus, which has been verified then with the help of Concurrency Workbench (CWB-NC) tool. Specifications in CCS have been verified against the requirements of the system using Mu-Calculus. It is motivated by a temporal logic specification. The main safety requirement of the crossing system is that there should never be a train and a car inside the crossing at the same time, which has been achieved in this paper by counting the number of cars entered into the crossing and number of cars left from the crossing through modeling. Before lowering the gate, the number of cars entered must be equal to the number of cars left. This main requirement of the crossing has been verified with the help of CWB-NC tool.