Abstract: In this study, we aimed at improving the performances of state space construction by using an efficient method to avoid state explosion problem in model checking through the use of-DBM (Difference Bounded Matrices) and on the fly strategy. This approach requires at any time, only the needed states to be in memory and allows for checking several properties, especially, safety, bounded liveness and temporal correctness, which are the most important ones in reactive systems. The specifications are expressed in timed automata and TCTL for the system and properties, respectively. The effectiveness of our approach has been demonstrated on many academic examples. The results obtained demonstrate that it is able to verify several properties that could not be checked by other state-of-the-art tools.
INTRODUCTION
Model checking is emerging as a practical tool for automated debugging of complex embedded systems. It is the most successful approach that's emerged for verifying requirements[1-3]. A model-checking tool accepts system requirements or design (called models) and a property (called specification) that the final system is expected to satisfy. In model checking, a high-level description of a system is compared against a logical correctness requirement to discover inconsistencies. The model checker will either terminate with the answer true, indicating that the model satisfies the specification, or false, indicating that the model does not satisfy the property and provides a counter example execution that shows an execution trace that violates the claim. Counter examples are one of the most useful features of model checking, as they allow users to quickly understand why a claim is not satisfied.
In this field, researchers are mainly faced with application complexity especially in the embedded systems domain. Among these is the state space explosion problem. The latter is the subject of most model checking research[4-7]. Usually, this problem results from the fact that the size of the state space is exponential in the number of variables and concurrent units in the system.
In this study, we provide an approach to reduce state space complexity and run time. It consists of an appropriate exploration on the fly, which is based on a data structure called DBM[3,8]. We model the system by timed automata and express requirements by TCTL (Timed Computation tree Logic)[9-11].
Preliminaries and state of the art: Here, we present the basic notions used in our approach.
Timed automata: Since their introduction by Alur et al.[3], timed automata were studied under multiple facets, both on the theory languages level and temporized models for specification and checking. Indeed, problems such as non-determinism, minimizing, the expressive power of clocks, and logical characterization of timed languages[7-10], were studied. This model was used successfully in the specification and the checking of timed systems, a large presentation was done by Dill[3]. Timed automata are Kripke structures with variables called clocks. Clocks are variables that evolve in time, all at the same speed, except the one that represents the universal time which is never set to zero. This general clock is often implicit.
Formally, a Kripke structure is a transition system M = <S, R, I, L, λ>. S consists of the set of possible states, I is the set of initial states I ⊆ S, R a set of transitions, R ⊆ S x S, L is a set of labels and λ an application of S in 2AP, which associates with each state an element of AP (AP: a set of atomic propositions).
A path in the Kripke model is an infinite sequence σ = s0, s1, s2, . . . ∈ S* , s0 ∈ I and (si si+1) ∈ R. A state s is reachable in M if there is a path from s.
TCTL: A temporal logic with timing: TCTL is the quantitative extension of CTL where, temporal modalities are subscripted with constraints on duration[4,12]. Formulae are interpreted over Timed Transition System (TTS).
TCTL formulae: These formulae are given by the following grammar:
| φ, ψ ::= P1 | P2 | . . . | |
| Aφ U~c ψ |
Where, ~ can be any comparator in {<,≤,=,≥,>}, c any natural number and Pi 0 AP.
Standard abbreviations: include T,
Semantics of TCTL: The following clauses define when a state s of some TTS T = (S, sinit,6, l) satisfies a TCTL formula n, written s |= φ, by induction over the structure of n (semantics of boolean operators is omitted).
Thus, in EφU~ c ψ, the classical until is extended by requiring that ψ be satisfied within a duration (from the current state) verifying the constraint ~ c .
Given a TA, A = <Q, C, qinit, →A, InvA, lA> and a TCTL formula φ, we write A |= φ when sinit |= φ.
Decision algorithm: One of the criteria of development for the model-checking is its decidability, i.e. it is possible to develop algorithms which calculate if the model of the system checks or not the property specification. There are varieties of algorithms according to the formalism used to model system[5] as well as the type of property and its specification language. The main criteria of development of these algorithms are mainly the effectiveness and the facility of implementation. Of course, the effectiveness is strongly related to the theoretical complexity of the problem of model-checking, but it is not equivalent. Moreover, the development of the algorithms goes with the importance of data structures for their implementation. These structures must be relatively compact.
Zone: In practice, verification tools for timed automata use regions, zones or BDD[6,9] for exploring the state space. A zone is a set of clock valuations definable by a conjunction o f constraints on the form x ~ c or x-y ~ c, where x a nd y are clocks, c is a constant, and ~ is one of the relational operators in {<;≤,≥;>}. A zone describes a union of several regions, and is thus a coarser representation of the state space. If we restrict the set of guards and invariants by disallowing negations, then we can easily restate the semantics of a timed automaton in terms of zones rather than clock valuations: A symbolic state is a pair (l; Z), where l is a location and Z is a zone. When computing the successor of a symbolic state, we first compute the effect of an edge by applying the guard of the edge and then projecting the zone according to the updates on the edge. Second we compute the future of the zone, i.e., the set of states which can be reached by delaying, and apply the invariant of the target location. Using zones, we obtain a countable representation of the state space. Here it becomes important to distinguish between diagonal-free and non-diagonal-free timed automata. The first class is the subset of timed automata where guards and invariants are limited to conjunctions of the form x ~ c, where, .~ 0 {<;≤;≥;>}. Shaw[13] has proven that for diagonal-free timed automata, we can construct abstractions and do all the operations effectively appearing in the algorithm.
Usaually the model-checker users simplify the model which they analyze, until being able to control it. That involves more distance between the model and the real system. It is difficult to manage this compromise. Currently, many theoretical researches seek to automate certain aspects of this simplification step.
The main problem of the algorithms of model-checking was the explosion of the number of states. This explosion occurs each time one decides to enumerate and to explicitly represent in memory all the states of the automaton examined. To surmount this obstacle, many techniques are used such as, the symbolic model-checking calling upon the zones to represent the sets of states.
SYMBOLIC MODEL CHECKING
In short, model checking is a collection of techniques for automated formal verification of finite-state concurrent systems. We start off with a bird’s eye view of the process (Fig. 1) and proceed to refine it in the following paragraphs[14,15].
Given a model (an abstraction of the system) and a specification of the properties that are required to hold (relating to absence of deadlocks, liveness, invariants etc.), the model checker verifies whether the former satisfies the latter. A counter example is produced upon discovery of a violation.
This approach uses an algorithm of symbolic model checking which calculates the unit characteristic of a formula TCTL i.e., the entire configurations i checked by this formula. The main problem of the symbolic approach relates to the procedure of decision.
| Fig. 1: | Model checking: a high level view |
Indeed, to decide if a set of states is included in another, we decide if a predicate implies another. In order to solve this problem, we propose a representation of the sets characteristic of the formulas which is at the base of a decision procedure implemented efficiently. The algorithm of symbolic model checking comprises four steps: 1) to represent the predicates of states, 2) to represent the temporal constraints in form matrix, 3) to calculate the operator>4) to evaluate symbolically the formulas of TCTL .
Being given a formula n of TCTL and a timed automaton, the symbolic algorithm consists in calculating for n the set S (n) of symbolic states which represents the characteristic set of n. Either A = (S, H, E, SI, δ, P) an timed automaton and n is a formula of TCTL, S (n) is built by induction on the structure of n such the following way:
Where: X0 = S (φ2) and Xk+1 = Xk ∨ S (φ1) ∇ Xk
Where: X0 = S (φ2) et Xk+1 = Xk
∨
and
| Table 1: | Model checking tools |
with
and
In order to implement this algorithm, a data structure is needed to represent zones and this data structure allows testing inclusion of zones and computing easily the different operations used in the algorithm, that is the intersection of two zones, the future of a zone, the image of a zone by a reset and the k-approximation of a zone. By using the automata theoretic approach to model checking, it is possible in many cases to avoid construction the entire state space of the modelled system. This is because the states of the automaton are generated only when needed, while checking the emptiness of its intersection with the property automaton. This tactic is called on-the-fly model checking[11,16,17].
Remark: This algorithm is implemented in some tools such as Knonos[11,18] and Uppaal[19].
Table 1 shows the main tools and their basic components as models (timed automata, Y), specification language (PLTL: propositional linear temporal logic, TCTL, Y) and exploration algorithms for reacheability analysis and specification checking[20].
EXPERIMENTAL RESULTS
To validate our tool, we chose three examples of embedded systems, the Mouse with only one button[13], temperature controller[8], train-gate controller and an abstract example[11]. To facilitate the comprehension and comparison, we have chosen often used examples in the literature.
TCTL properties: We have not only focused on safety properties that constitute the majority of properties required to verify systems, but also on other important ones such as the bounded liveness and temporal correctness properties. Bounded liveness property guarantees that something will take place with giving the deadline information. Temporal correctness property avoids deadlock situations.
Temporal correctness property: It is stated as follows:
| φ = (EFw = constant > 0, tested on the example 1. |
The temporal correctness property is used to check that the system is well modeled i.e. one cannot reach a state of deadlock. This deadlock might occur when the temporal constraints are not expressed correctly. For example, an invariant of state 0 is x≤5, the condition of transition from the state 0 to the state 1 is x < 3. In the state 0, the system can remain no later than 5 time units. If the system remains in the state 0 more than 3 time units, it cannot fire the transition between states 0 and 1. This situation is a deadlock. It must be corrected. An example of such situation is given here.
Bounded liveness property: For the mouse, we wish to check the following property: if the button in a hurry and were slackened once then inevitably before a time equal with tcs+ tcd , the system detects a simple click or a double click. This property is expressed in TCTL by the formula:
Safety property: The specification of the controller is established for reasons of safety. If the controller does not receive a new order of refrigeration before a time tmax since the last order received, then it must also refrigerate. This property is expressed by the following formula:
This means that it is not possible to reach a state which satisfies r in a time more than 35 time units, starting from a state which satisfies r without passing by a state which satisfies b.
Bounded liveness and safety properties are likely applied on the train-gate controller exemple.
Results
The results given by SYMTC are synthesized on Table 2. We can deduce that the complexity of the model- checking is a function of the parameters such as the number of model states, the number of clocks and the type of the property to be checked. We show here three examples, which exhibit different characteristics (in terms of number of states, number of clocks). For the mouse model, the obtained results (satisfied property or not) for the bounded liveness property is the same as those shown Yovine[11] and Shaw[13]. For the temperature controller’s model, the positive result of safety property is identical to that obtained Jaffe et al.[8] while the other obtained results are specific to our tool and can be used as a basis of comparison in research works.
Table 3 shows the comparison between the regions and symbolic approaches. It is worth noting that the gain on the memory space is very important; it goes from 20 to 8547 times less.
Compared to the region’s method, our approach reduces at a large extent, both the required memory size and the execution time. Firstly, we explore all the model states by saving the state invariants in a matrix, next, we execute the algorithm at every matrix entry consultation to recover the data. This will allow us to avoid exploration of the whole graph. Secondly, to reduce the memory size, we use the characteristic set concept or zone.
On the other hand, in contrast to other similar extensions, we have used TCTL that has two main advantages: it is based on traditional structures of kripke [Kripke] and the model checking is done in polynomial time. In addition to its similarity with Kronos[19], SYMTC has a graphic interface of timed models and a simulation module, but it is not limited in reachability property, like UPPAAL[19]. Furthermore, our approach allows more properties to be checked such as the safety, bounded liveness, and correctness ones, etc.
CONCLUSIONS AND FUTURE WORK
In this study, we proposed an approach to handle the memory explosion problem in symbolic model checking through the use of timed automata for embedded systems model. The approach allows for checking various important properties like safety, bounded liveness, and temporal correctness.
| Table 2: | Recapitulative table of the results obtained by the SYMTC Checker |
| Table 3: | A comparison between regions and symbolic approach |
To this end, we used DBM representation that brings a significant advantage due to its ability to control the memory required. This approach is based on the fly invariant checking and checking TCTL formulas expressible as least fix point. Another distinctive feature of our approach relies in the use of dynamic cache that brings more state space exploration speedups.
Compared to state of the art techniques, experimental results of our approach, show that it scales very well, and reduces the memory required without affecting results quality and performance.
Future work would focus on varied verification application domains, where state of the art model checkers are not very efficient. We also plan to extend the technique to verify more varied and complex properties. There are a number of other ways that model checkers can be improved to make them easier to use by engineers. One problem with current systems is how to make the specification language more expressive and easier to use. Some type of timing diagram notation may be more natural for engineers than TCTL. One trend for research is to develop even more concise techniques for representing Boolean functions. When better representations are developed, they can easily be incorporated into model-checking algorithms. Other direction is in investigation Model Checking techniques combined with very different styles of reasoning into a single framework. The problem is how to combine and can smoothly integrate the results obtained by each.