É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 metadatas

Cited literature [10 references]  Display  Hide  Download

https://hal.inria.fr/hal-01665717
Contributor : Annie Ressouche <>
Submitted on : Saturday, December 16, 2017 - 5:08:29 PM
Last modification on : Tuesday, April 2, 2019 - 9:54:05 PM

File

RapportFinalDorine.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01665717, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

217

Files downloads

104