Skip to Main content Skip to Navigation
Master thesis

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

Abstract : 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.
Document type :
Master thesis
Complete list of metadata

Cited literature [10 references]  Display  Hide  Download
Contributor : Annie Ressouche Connect in order to contact the contributor
Submitted on : Saturday, December 16, 2017 - 5:08:29 PM
Last modification on : Saturday, June 25, 2022 - 11:28:44 PM


Files produced by the author(s)


  • HAL Id : hal-01665717, version 1



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⟩



Record views


Files downloads