Event
MBSE Colloquium: Jeroen Keiren, "Model checking to improve quality of complex industrial software"
Monday, July 11, 2016
11:00 a.m.
1146 AV Williams Building
Kimberly Edwards
kedwards@umd.edu
Model-Based Systems Engineering Colloquium
Using model checking to improve the quality of complex industrial software
Jeroen Keiren
Assistant Professor for Software Engineering
Open University of the Netherlands
Abstract
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.
Biography
Dr. Jeroen Keiren is assistant professor for Software Engineering at the Faculty of Management, Science and Technology of the Open University of the Netherlands (OUNL). He is also affiliated with the Radboud University in Nijmegen as a member of the Digital Security department of the Institute for Computing and Information Sciences. Keiren obtained his PhD from Eindhoven University of Technology in 2013. He has experience in formal methods and software verification research, in particular model checking. He is also experienced in applying model checking tools in an industrial context, for example in verifying the configuration phase of the IEEE 11073-20601 protocol for medical devices, and the analysis of the detector controls software of the CMS detector in the large hadron collider (LHC) at CERN.
