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

Résumé : 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.
Type de document :
Mémoires d'étudiants -- Hal-inria+
Informatique et langage [cs.CL]. 2017
Liste complète des métadonnées

Littérature citée [11 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01665717
Contributeur : Annie Ressouche <>
Soumis le : samedi 16 décembre 2017 - 17:08:29
Dernière modification le : lundi 18 juin 2018 - 23:10:04

Fichier

RapportFinalDorine.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01665717, version 1

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〉

Partager

Métriques

Consultations de la notice

157

Téléchargements de fichiers

48