Developing correct parallel and distributed software is a daunting task. The parallelism causes the state-spaced explosion problem: the number of states in the system grows exponentially with the number of parallel components. One of the ways to verify that such a system satisfies its requirements is model checking.
In this talk, I will describe the application of model checking to two real-world systems, and describe the errors that were uncovered using this approach.
The first system is the session setup protocol that is part of the IEEE 11073-20601:2008 standard for communication between personal health devices. I describe issues present in that standard, and share some general observations on standards describing communication protocols.
The second system I describe is detector control system of the CERN Compact Muon Solenoid experiment (part of the Large Hadron Collider). This system consists of 27,500 nodes, and the software of each of these nodes is implemented as a finite state machine. The sheer size of the system, estimated to consist of at least 10^27,500 states, makes it impossible to fully understand the details of the system behavior at the macro level. We have formally described the finite state machines, and implemented an automatic translation to the mCRL2 process algebra. Correctness of the translation was assessed by means of simulation and visualization of individual finite state machines, and through formal verification of complete subsystems of the control software. Based on the formalized semantics of the finite state machines, specific verification questions were translated to satisfiability problems to allow for efficient solving, enabling verification of the complete system in minutes. The IDE that is used for developing the FSMs has been extended with the verification technology.
Dr. Keiren is a Dutch assistant professor, he is working on adapting a generalized approach to model checking based on equation-solving to the analysis of hybrid systems (CyberCardia applications). Jeroen was a student of Jan Friso Groote’s at Eindhoven and currently has appointments at Nijmegen and the Open University in the Netherlands.