MODEL CHECKING --- A HANDS-ON INTRODUCTION

Model Checking is a formal technique for the verification of designs of concurrent systems. It is based on the representation of the system being analyzed as a (finite state) transition systems (e.g. Kripke models), while the requirements are typically expressed in temporal logics. A system satisfies a given property amounts to checking if the corresponding temporal formula is true in the Kripke model. Model checking is very effective in pinpointing design errors that are extremely hard to detect by means of testing, and is therefore being applied in the industrial development of reactive systems, hardware designs, and communication protocols. Furthermore, model checking techniques and tools are gaining interest in several fields of Artificial Intelligence (e.g. Planning, Multi-agent systems, and Model-based Diagnosis) and Engineering (e.g. Requirement Verification, Safety Analysis). Of particular interest is Symbolic Model Checking, which makes it is possible to analyze extremely large finite-state systems by means of symbolic representation techniques (e.g. Binary Decision Diagrams, propositional satisfiability).

Information about the authors

Alessandro Cimatti is the leader of the formal methods group within the Automated Reasoning Systems division (SRA) at ITC-IRST. The activities carried out by the group include basic research, the development of the NuSMV model checker, and technology transfer in industrial projects in the areas of safety critical applications (e.g., railways, avionics, aerospace, industrial plant controllers). Alessandro Cimatti has participated in and led several industrial projects aimed at the use of formal methods for the development and verification of safety critical systems and embedded controllers. Some examples are the validation of Interlocking Systems, the development of Rail Traffic Management Systems, the design of tools for on-board verification, and the verification of safety-critical communication protocols. Alessandro Cimatti is the leader of the development of NuSMV. His main research interests include the development of advanced model checking techniques, and the application of model checking for the synthesis of reactive controllers and test cases. He has also contributed to the research in theorem proving, formal languages for the specification of multi-agent systems, planning and robotics.

Marco Pistore is Associate Professor at the Department of Information and Communication Technologies of the University of Trento and Research Consultant at ITC-IRST. His research interests are in formal methods and in the application of formal methods to planning and to synthesis of controllers. Marco Pistore has been the responsible of the development of the NuSMV model checker. He is also working to the Formal Tropos project, aiming at the development of a formal language and of formal analysis techniques for the verification of requirements specifications. Marco Pistore has also participated to research and industrial projects on the application of formal methods to the design and verification of safety-critical systems and of embedded controllers.

Marco Roveri received a PhD in Computer Science in 2002 from the University of Milano in collaboration with ITC-Irst under the supervision of A. Cimatti. His PhD thesis "Planning in Non-Deterministic Domains via Symbolic Model Checking" was awarded by the Italian Association for Artificial Intelligence (AI*IA) the best price for PhD thesis in artificial intelligence in Italy. He his in the steering committee of the NuSMV symbolic model checker, the first state-of-the-art open source symbolic model checker. Since 2001 he is working at ITC-Irst in the Automated Reasoning Systems division. From 1997 until 2002 he was collaborating with ITC-Irst on topics related to Artificial Intelligence Planning and Formal Verification. His research interest are: integration of formal verification techniques along the whole software development process, planning in non-deterministic domains under different assumptions on run-time observability using symbolic model checking techniques and symbolic model checking.

back to tutorials list