Article Preview
TopIntroduction
The development of critical systems, such as systems whose failure can have catastrophic consequences, requires the use of reliable design methods based on formal approaches. These later allow the precise description of systems and their desired properties, as well as reasoning about them. The systems are modeled in a language with clear mathematically defined syntax and semantics, like logics, automata and process algebra.
In this paper we are interested by a subclass of timed automata model, named timed automata with durational actions (daTA). The daTA model (Belala et al., 2013; Guellati et al., 2014) are a form of timed automata that admit a more natural representation of action durations and advocates carrying true concurrency, which are realistic assumptions for specifying real-time systems. It’s based on maximality semantics.
Indeed, in real world systems, actions are not instantaneous, but have durations. This realistic characteristic is important in many cases in addition to the maximality semantics has been proved necessary and sufficient both for the refinement process and duration of actions (Saïdouni & Courtiat, 2003).
One of the most automated tool in formal verification is Model Checking (Holzmann, 1991), where a finite state space of a system is constructed and the desired correctness properties are checked against it. Generation phase consists on exploring all possible reached states from the initial state.
Actually, a large part of real-life systems are made up of many interacting components, for which state space can be huge and eventually cannot fit in memory or even be, it will be too large for being explored entirely. This leads to the so called state space explosion problem, which is known to be the most limiting and decreasing factor of this technique.
Several approaches have been developed to cope with this issue, such as symbolic state space encoding using binary decision diagram (BDD) (Drechsler & Becker, 1998; Heyman et al., 2000), other method have taken benefits from some equivalence relations to reduce the state space of the model, like: partial order reduction (Godefroid & Wolper, 1994), bisimulation relation (Blom & Orzan, 2005), alpha-equivalence relation (Bouneb & Saidouni, 2009) and aggregation (Saidouni et al., 2011).
As recent researches are based on the use of parallel and distributed computations, many papers presenting distributed model checking algorithms mention the importance of a good state space partitioning method. A good partitioning scheme can efficiently reduce the problem of the combinatorial state space explosion (Garavel et al., 2001; Barnat et al., 2001; Bingham et al., 2010; Voros et al., 2011), all these approaches consist on the use of a cluster or a network of workstations and each machine explores a part of the state space. However, they bear differences on the memory architecture used; either shared or distributed one, the data structure selected to store states, and the way sates are distributed over machines of the network.
In this paper, our contributions are of interest for the formal verification domain and more especially for the distributed Model Checking. In its first step, Model Checking consists on generating the full state space: starting from the initial state, computes all its successors, repeats the process for all the newly discovered states until achieving exploration; there is no more state to explore. The fundamental interest of this proposal is the construction of distributed state space in the context of the maximality semantics based on zones using distributed hash tables structure.
We propose a novel approach to construct a zone graph, based on the maximality semantics called Maximality-based Zone Graph (MZG) and we define Timed Maximality Bisimulation Relation (TMBR) for real-time model based on the maximality semantics.