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

Annie Ressouche (1) , Daniel Gaffé (2) , Dorine Havayarimana (3)

1 STARS - Spatio-Temporal Activity Recognition Systems
2 LEAT - Laboratoire d'Electronique, Antennes et Télécommunications
3 UNS - Université Nice Sophia Antipolis (1965 - 2019)

Model verification, more commonly known as Model Checking, is a concept based on an automatic formal verification approach of temporal properties on reactive systems. INRIA in collaboration with LEAT developed CLEM, a modeling and property verification tool, based on a state representation in finite automata generated automatically using binary decisions diagrams. From an evolutionary point of view, the work carried out during this internship was to develop the library of linear decisions diagrams, 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 the verification part of CLEM by replacing the representation of the fundamental values using binary decisions diagrams(BDDs) with linear decisions diagrams(LDDs) which will allow us to represent the states by integer values instead of signals which are not comparable among themselves. This new library, once implemented on CLEM, will make checks of finer models and, we hope, will make it more powerful.

La vérification de modèle, plus communément appelé Model Checking, est un concept basé sur une approche automatique de vérification formelles des propriétés temporelles sur 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 une représentation d’état en automates finis générés automatiquement et représentés par des Diagrammes de Décisions Binaires. Dans une optique d’évolution, le travail effectué durant ce stage a été de développer la bibliothèque de diagramme de décision linéaire, nous nous sommes concentrés sur l’inclusion de nouvelles méthodes de réduction dans les cas d’implication forte et faible. L’objectif de ce travail est de développer la partie vérification de CLEM en remplaçant la représentation actuelle des valeurs fondamentales qui utilisent des diagrammes de décisions binaires(BDDs) par les diagrammes de décisions linéaires(LDDs) ce qui nous permettrait de représenter les é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, permettra de faire des vérifications de modèles plus fines et, potentiellement, le rendra plus performant.

Domaines: Informatique et langage [cs.CL]

Annie Ressouche, Daniel Gaffé, Dorine Havayarimana. Études et développement de diagrammes de décision linéaires. Informatique et langage [cs.CL]. 2017. ⟨hal-01665717⟩