Implementation of an environment of symbolic model checking based on the TDGs

Summary form only given. Several applications generate complicated finite states systems as the design of the communications protocols and the design of circuits. When the number of states of a system is large, it is difficult to determine manually if such a system is correct or not. The checking or model checking proposed in parallel by both (Clarke and Emerson, Quielle and Sifakis) is a method to decide automatically if a finite states system satisfies or not its specifications. This algorithm is called model checking. In symbolic model checking of finite state systems, the general approach is based on BDDs (binary decision diagrams) representation, proposed by Bryant. However, the problem of the explosion of the space of states therefore is not solved in an effective way. Also, the construction of the BDDs proves sometimes difficult in some applications, in particular in software applications. For the static analysis of programs, another model of symbolic notation, the TDGs (typed decision graphs), was proposed by Mauborgne. We show that, in this context, the TDGs bring a considerable profit of capacity memory compared to the BDDs. This reduction of the complexity of the representation lets hope for an improvement of the execution times. Thus, we use this symbolic representation for our environment of verification and we attempt to improve executions time of verifications programs. We detail the approach of symbolic representation of the finite states systems: the set of states and the transition relation with our method of construction of TDGs from the logical operations. To specify the behaviour of a system according to the passing of the time, we are interested to the temporal logic CTL(computational tree logic), that allows the expression of the properties of the branching time. We apply that on the example of the 3-bit counter. Then, we illustrate the example of processes using a variable semaphore to implement mutual exclusion. Hence, the motivation of our- research which is about the development of an environment of symbolic model checking based on TDGs. In a future work, we are interested to apply this environment for the checking of the real applications and to compare its performances with the existing tools for checks.