Exploration implicite et explicite de l'espace d'´etats atteignables de circuits logiques Esterel

摘要

This thesis deals with implicit and explicit approaches, as well as the convergence of these approaches, to the reachable state space exploration of logical circuits generated from synchronous reactive programs written in Esterel, ECL or SyncCharts. Our work aim at reducing the cost of these explorations either by the way of generic techniques or techniques that are specific to our context. We apply the results of these explorations to formal verification of safety properties, explicit automaton generation or exhaustive test sequence generation. We describe three tools.The first tool is an implicit formal verifier based on Binary Decision Diagrams (BDDs). This verifier provide several techniques aiming at reducing the number of variables that are involved in reachable state space computations. We provide in particular a variable abstration technique based on the use of a trivalued logic. This new technique extends the usual technique in which state variables are replaced by free inputs. As these two techniques compute over-approximations of the reachable state space, we provide several methods aiming at reducing this over-approximation by using structural information concerning the model.The second tool is an explicit exploration engine based on the enumeration of reachable states. This engine is based on the simulation of the electric current propagation within the circuit and it provides transparent support for cyclic circuits. This engine includes numerous optimisations and uses several heuristics aiming at avoiding explosions in time or space which are inherent to this approach, thus providing very good performances. This engine has been applied to explicit automaton generation and formal verification.Finally, the third tool is an hybrid implicit/explicit evolution of the pure explicit engine. In this version, states are still analyzed one by one but in a symbolic way, using BDDs. This engine has also been applied to explicit automaton generation and formal verification as well as exhaustive test sequence generation.We present experiment results of these different approaches on several industrial examples.