Author/Authors
ferdenache, ahlem université badji mokhtar - laboratoire de systèmes embarqués –lase, Algérie , boudour, rachid université badji mokhtar - laboratoire des systèmes embarqués(lase), Algérie
Title Of Article
Un vérificateur symbolique efficace
شماره ركورد
31249
Abstract
En génie informatique d’aujourd’hui, l’objectif est d’arriver à des méthodes et des outils qui peuvent exécuter la vérification de modèle automatiquement : le model checking. Le problème du model checking est le grand espace d’états. Une des solutions est d’utiliser le model checking symbolique combinée à des structures de données compactes. Le but de ce papier est de concevoir et mettre en application un nouvel outil performant, pour vérifier des propriétés importantes dans les systèmes critiques basés sur la notion d’état symbolique ainsi que des structures de données DBM (Difference Bound Matrices). Les spécifications sont exprimées à l’aide d’automates temporisés pour le système et de logique temps réel pour les propriétés. Les résultats obtenus sont comparés à ceux de la littérature.
From Page
94
NaturalLanguageKeyword
vérification symbolique , automates temporisés , TCTL–à la volée , DBM
JournalTitle
Revue Des Sciences Et De La Technologie, Synthèse
To Page
105
JournalTitle
Revue Des Sciences Et De La Technologie, Synthèse
Link To Document