Modeling and Formally Verifying a Safety-Critical System Through MCRL2

Software testing is a method for finding bugs in programs for a long time. Software model checking is a better alternative of software testing that does not only find bugs in the software but also proves absence of bugs in the software. Model checking is a technique for automatically verifying the correctness of the 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”. Many successful tools for software model checking exist today. The specifications of the model are expressed in “mCRL2” which is a formal specification language with an associated toolset. The toolset can be used for modeling, validation and verification of concurrent systems and protocols. The requirements of the system are written in the form of properties or formula in μ-Calculus (called as Mu-calculus), which has been verified with the help of mCRL2. It is motivated by a temporal logic specification. One of the main safety requirements of the level-crossing control system is that a train and a car should never be inside the crossing at the same time, which is verified in this paper by comparing the number of cars entered into the crossing and number of cars left from the crossing through modeling. One more critical requirement of the system is the gate will be lowered only when the number of cars entered must be equal to the number of cars left. This main requirement of the crossing has been also verified with the help of mCRL2 verification tool.