Model checking concurrent and real-time systems : the PAT approach

Abstract

The design and verification of concurrent and real-time systems are notoriously difficult problems. Among the software validation techniques, model checking approach has been proved to be successful as an automatic and effective solution. In this thesis, we study the verification of concurrent and real-time systems using model checking approach. <br><br> First, we design an integrated formal language for concurrent and real-time modeling, which combines high-level specification languages with mutable data variables and low-level procedural codes for the purpose of efficient system analysis, in particular, model checking. Timing requirements are captured using behavior patterns like <I>deadline</I>, <I>time out</I>, etc. A formal semantic model is defined for this language. <br><br> Based on this modeling language, we investigate LTL verification problem with focus of fairness assumptions, and refinement checking problem with following results. <UL> <LI> We propose a unified on-the-fly model checking algorithm to handle a variety of fairness assumptions, which is further tuned to support parallel verification in multi-core architecture with shared memory. We apply the proposed algorithm on a set of self-stabilizing population protocols, which only work under global fairness. One previously unknown bug is discovered in a leader election protocol. Population protocols are designed for networks with large or even unbounded number of nodes, which gives the space explosion problem. To solve this problem, we develop a process counter abstraction technique to handle parameterized systems under fairness. We show that model checking under fairness is feasible, even without the knowledge of process identifiers. <br><br> <LI> Based on the ideas in FDR, we present a on-the-fly model checking algorithm for refinement checking, incorporated with advanced model checking techniques. This algorithm is successfully applied in automatic linearizability verification and conformance checking between Web Services. </UL> <br> Symbolic model checking is capable of handling large state space. We present an alternative solution for LTL verification using bounded model checking approach. Hierarchical systems are encoded as SAT problems. The encoding avoids exploring the full state space for complex systems so as to avoid state space explosion. <br><br> To support verification of real-time systems, we propose an approach using a fully automated abstraction technique to build an abstract finite state machine from the real-time model. We show that the abstraction has finite state and is subject to model checking. Furthermore, it weakly bi-simulates the concrete model and we can perform LTL model checking, refinement checking and even timed refinement checking upon the abstraction. <br><br> The results of this thesis are embodied in the design and implementation of a self-contained framework: <a href="http://pat.comp.nus.edu.sg/">Process Analysis Toolkit (PAT)</a>, which supports composing, simulating and reasoning of concurrent and real-time systems. This framework includes all of the proposed techniques: deadlock-freedom, reachability, LTL checking, refinement checking and etc. PAT adopts an extensible design, which allows new languages and verification algorithms to be supported easily. Currently, three modules have been developed in PAT. The experiment results show that PAT is capable of verifying systems with large number of states and complements the state-of-the-art model checkers in several aspects.