Efficient symbolic model checking of concurrent systems
Loading...
Journal Title
Journal ISSN
Volume Title
Perustieteiden korkeakoulu |
Doctoral thesis (article-based)
Checking the digitized thesis and permission for publishing
Instructions for the author
Instructions for the author
Unless otherwise stated, all rights belong to the author. You may download, display and print this publication for Your own personal use. Commercial use is prohibited.
Author
Date
2011
Major/Subject
Mcode
Degree programme
Language
en
Pages
Verkkokirja (2483 KB, 94 s.)
Series
Aalto University publication series DOCTORAL DISSERTATIONS ,
111/2011
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.Description
Supervising professor
Niemelä, Ilkka, Prof.Thesis advisor
Junttila, Tommi, Dr.Keywords
software verification, distributed systems, bounded model checking, UML, predictable abstraction
Parts
- [Publication 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.
- [Publication 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.
- [Publication 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.
- [Publication 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.
- [Publication 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.
- [Publication 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.
