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 highlevel 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 softwareintensive 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.
Translated title of the contribution  Efficient symbolic model checking of concurrent systems 

Original language  English 
Qualification  Doctor's degree 
Awarding Institution 

Supervisors/Advisors 

Publisher  
Print ISBNs  9789526043487 
Electronic ISBNs  9789526043494 
Publication status  Published  2011 
MoE publication type  G5 Doctoral dissertation (article) 
Keywords
 software verification
 distributed systems
 bounded model checking
 UML
 predictable abstraction
Fingerprint Dive into the research topics of 'Efficient symbolic model checking of concurrent systems'. Together they form a unique fingerprint.
Cite this
Dubrovin, J. (2011). Efficient symbolic model checking of concurrent systems. Aalto University. http://urn.fi/URN:ISBN:9789526043494