Abstract
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 tri-valued 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.
Résumé
Cette thèse traite des approches implicites et explicites, ainsi que de leur convergence, de l'exploration d'espace d'états atteignables de circuits logiques provenant de programmes réactifs synchrones écrits en Esterel, ECL ou SyncCharts. Nos travaux visent à réduire les coûts de ces explorations à l'aide de techniques génériques ou spécifiques à notre cadre de travail. Nous utilisons les résultats de ces explorations à des fins de vérification formelle de propriétés de sûreté, de génération d'automates explicites ou de génération de séquences de tests exhaustives. Nous décrivons trois outils.
Le premier outil est un vérificateur formel implicite, à base de Diagrammes de Décisions Binaires (BDDs). Ce vérificateur présente plusieurs techniques permettant de réduire le nombre de variables impliquées dans les calculs d'espace d'états. Nous proposons notamment l'abstraction de variables à l'aide d'une logique trivaluée. Cette nouvelle méthode étend la technique usuelle de remplacement de variables d'états par des entrées libres. Ces deux méthodes calculant des sur-approximations de l'espace d'états atteignables, nous proposons différentes techniques utilisant des informations concernant la structure du modèle et permettant de réduire la sur-approximation.
Le deuxième outil est un moteur d'exploration explicite, basé sur l'énumération des états accessibles. Ce moteur repose sur la simulation de la propagation du courant électrique dans les portes du circuit et supporte les circuits cycliques. Ce moteur comporte de nombreuses optimisations et fait appel à différentes heuristiques visant à éviter les explosions en temps ou en espace inhérentes à cette approche, ce qui lui confère de très bonnes performances. Ce moteur a été appliqué à la génération d'automates explicites et à la vérification formelle.
Enfin, le troisième outil est une évolution hybride implicite/explicite du moteur purement explicite. Dans cette évolution, les états sont toujours analysés individuellement mais symboliquement à l'aide de BDDs. Ce moteur a également été appliqué à la génération d'automates explicites, mais il est plutôt destiné à la vérification formelle ou la génération de séquences de tests exhaustives.
Nous présentons des résultats d'éxpérimentations de ces différentes approches sur plusieurs exemples industriels.
| Home/Accueil 
- (Plzen, Czech Republic, June 2, 2004)
Slides
