Publications

In this paper, we propose a hybrid parallel model checking algorithm for both shared and distributed memory architectures. The model checking is performed simultaneously with a parallel construction of system state space by distributed multi-core machines. The represen- tation of the system’s state space is a hybrid graph called Symbolic Ob- servation Graph (SOG), which combines the symbolic representation of its nodes (sets of single states) and the explicit representation of its arcs. The SOG is adapted to allow the preservation of both state and event- based LTL formulae (hybrid LTL), i.e. the atomic propositions involved in the formula to be checked are either state or event-based propositions. We have implemented the proposed model checker within a C++ proto- type and compared our preliminary results to the LTSmin model checker.

The model checking is one of the major techniques used in the formal verification. This technique builds on an automatic procedure that takes a model M of a system and a formula φ expressing a temporal property, and decides whether the system satisfies the property (denoted by M|=φ). The model checking technique is based on an exhaustive exploration of the state space of the system and, thus suffers from the state space explosion problem: it can happen that the verification process stops because of lack of time or space. Among the existing solutions to tackle this problem the Symbolic Observation Graph(SOG) has been proposed as a reduced representation of the reachability graph preserving linear temporal logic properties (LTL) i.e. checking an LTL property on the SOG is equivalent to check it on the original state space. The parallel construction of the SOG could increase the speedup and scalability of model checking. In this paper, we propose a new model checking algorithm built on a parallel construction of the SOG. The SOG is adapted to allow the preservation of both state and event-based LTL formulae i.e., the atomic propositions involved in the formula to be checked could be either state-based or event-based propositions. We implemented the proposed model checking algorithm within a C++ prototype and compared our preliminary results with the state of the art model checkers.

The model checking is one of the major techniques used in the formal verification. This technique takes a model of a system in question and decides whether it satisfies a given property or not. It is based on an exhaustive exploration of the state space of the system to be verified. Thus, the Model checking technique suffers from the state space explosion problem. It can happen that the verification process stops because of lack of memory space. One solution is to reduce state space representation by using a symbolic representation such as symbolic observation graphs. Using symbolic graphs requires more intensive computations that induces a drastic increase in runtime. In order to reduce runtime, we propose to parallelize the verification process. The use of distributed processing increases the speedup and scalability of model checking by exploiting the cumulative computational power and memory of a cluster of computers. Such approaches have been studied in various contexts leading to different proposed solutions for both symbolic and explicit model checking. In this thesis, we propose a new model checking algorithms built on a parallel construction of the Symbolic Observation Graph: an abstraction of the state space graph that preserves Linear Temporal Logic (LTL). We implemented the proposed model checking algorithms within a C++ prototype and compared our preliminary results with the state of the art model checkers.