The doctoral dissertations of the former Helsinki University of Technology (TKK) and Aalto University Schools of Technology (CHEM, ELEC, ENG, SCI) published in electronic format are available in the electronic publications archive of Aalto University - Aaltodoc.
Aalto

Efficient Symbolic Model Checking of Concurrent Systems

Jori Dubrovin

Doctoral dissertation for the degree of Doctor of Science in Technology to be presented with due permission of the School of Science for public examination and debate in Auditorium TU1 at the Aalto University School of Science (Espoo, Finland) on the 18th of November 2011 at 12 noon.

Overview in PDF format (ISBN 978-952-60-4349-4)   [2483 KB]
Dissertation is also available in print (ISBN 978-952-60-4348-7)

Abstract

Design errors in software systems consisting of concurrent components are potentially disastrous, yet notoriously difficult to find by testing. Therefore, more rigorous analysis methods are gaining popularity. Symbolic model checking techniques are based on modeling the behavior of the system as a formula and reducing the analysis problem to symbolic manipulation of formulas by computational tools. In this work, the aim is to make symbolic model checking, in particular bounded model checking, more efficient for verifying and falsifying safety properties of highly concurrent system models with high-level data features.

The contributions of this thesis are divided to four topics. The first topic is symbolic model checking of UML state machine models. UML is a language widely used in the industry for modeling software-intensive systems. The contribution is an accurate semantics for a subset of the UML state machine language and an automatic translation to formulas, enabling symbolic UML model checking.

The second topic is bounded model checking of systems with queues. Queues are frequently used to model, for example, message buffers in distributed systems. The contribution is a variety of ways to encode the behavior of queues in formulas that exploit the features of modern SMT solver tools.

The third topic is symbolic partial order methods for accelerated model checking. By exploiting the inherent independence of the components of a concurrent system, the executions of the system are compressed by allowing several actions in different components to occur at the same time. Making the executions shorter increases the performance of bounded model checking. The contribution includes three alternative partial order semantics for compressing the executions, with analytic and experimental evaluation. The work also presents a new variant of bounded model checking that is based on a concurrent instead of sequential view of the events that constitute an execution.

The fourth topic is efficient computation of predicate abstraction. Predicate abstraction is a key technique for scalable model checking, based on replacing the system model by a simpler abstract model that omits irrelevant details. In practice, constructing the abstract model can be computationally expensive. The contribution is a combination of techniques that exploit the structure of the underlying system to partition the problem into a sequence of cheaper abstraction problems, thus reducing the total complexity.

This thesis consists of an overview and of the following 6 publications:

  1. Jori Dubrovin and Tommi Junttila. Symbolic Model Checking of Hierarchical UML State Machines. In Application of Concurrency to System Design, 8th International Conference (ACSD 2008), pages 108-117, June 2008. © 2008 Institute of Electrical and Electronics Engineers (IEEE). By permission.
  2. Tommi Junttila and Jori Dubrovin. Encoding Queues in Satisfiability Modulo Theories Based Bounded Model Checking. In Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference (LPAR 2008), pages 290-304, November 2008. © 2008 Springer-Verlag. By permission.
  3. Jori Dubrovin and Tommi Junttila and Keijo Heljanko. Symbolic Step Encodings for Object Based Communicating State Machines. In Formal Methods for Open Object-Based Distributed Systems, 10th IFIP WG 6.1 International Conference (FMOODS 2008), pages 96-112, June 2008. © 2008 International Federation for Information Processing (IFIP). By permission.
  4. Jori Dubrovin and Tommi Junttila and Keijo Heljanko. Exploiting Step Semantics for Efficient Bounded Model Checking of Asynchronous Systems. Accepted for publication in Science of Computer Programming, Special Issue on Automated Verification of Critical Systems, 27 pages, available online 23 July 2011. © 2011 Elsevier. By permission.
  5. Jori Dubrovin. Checking Bounded Reachability in Asynchronous Systems by Symbolic Event Tracing. In Verification, Model Checking, and Abstract Interpretation, 11th International Conference (VMCAI 2010), pages 146-162, January 2010. © 2010 Springer-Verlag. By permission.
  6. Alessandro Cimatti and Jori Dubrovin and Tommi Junttila and Marco Roveri. Structure-Aware Computation of Predicate Abstraction. In Formal Methods in Computer Aided Design, 9th International Conference (FMCAD 2009), pages 9-16, November 2009. © 2009 Institute of Electrical and Electronics Engineers (IEEE). By permission.

Keywords: software verification, distributed systems, bounded model checking, UML, predicate abstraction

This publication is copyrighted. You may download, display and print it for Your own personal use. Commercial use is prohibited.

© 2011 Aalto University

Last update 2012-02-16