Études et développement de diagrammes de décision linéaires

Description

Model verification, more commonly known as Model Checking, is a concept basedon an automatic formal verification approach of temporal properties on reactive systems.INRIA in collaboration with LEAT developed CLEM, a modeling and propertyverification tool, based on a state representation in finite automata generated automaticallyusing binary decisions diagrams. From an evolutionary point of view, thework carried out during this internship was to develop the library of linear decisionsdiagrams, we focused on the implementation of new reduction methods in cases of"Imply High" and "Imply Low" case. The objective of this work is to develop theverification part of CLEM by replacing the representation of the fundamental valuesusing binary decisions diagrams(BDDs) with linear decisions diagrams(LDDs) whichwill allow us to represent the states by integer values instead of signals which arenot comparable among themselves. This new library, once implemented on CLEM,will make checks of finer models and, we hope, will make it more powerful.

Abstract (French)

La vérification de modèle, plus communément appelé Model Checking, est un conceptbasé sur une approche automatique de vérification formelles des propriétés temporellessur des systèmes réactifs. INRIA en collaboration avec le LEAT ont développéCLEM, un outil de modélisation et de vérification de propriétés, s'appuyant sur unereprésentation d'état en automates finis générés automatiquement et représentés pardes Diagrammes de Décisions Binaires. Dans une optique d'évolution, le travaileffectué durant ce stage a été de développer la bibliothèque de diagramme de décisionlinéaire, nous nous sommes concentrés sur l'inclusion de nouvelles méthodes deréduction dans les cas d'implication forte et faible. L'objectif de ce travail est de développerla partie vérification de CLEM en remplaçant la représentation actuelle desvaleurs fondamentales qui utilisent des diagrammes de décisions binaires(BDDs) parles diagrammes de décisions linéaires(LDDs) ce qui nous permettrait de représenterles états par des valeurs entières et non par des signaux non comparables entre eux.Cette nouvelle bibliothèque de LDDs, une fois implémentée sur CLEM, permettrade faire des vérifications de modèles plus fines et, potentiellement, le rendra plusperformant.

Abstract

National audience

Additional details