Synthèse
Volume 22, Numéro 2, Pages 94-105
2016-10-30

Un Vérificateur Symbolique Efficace



Auteurs : Ferdenache Ahlem . Boudour Rachid .

Résumé

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.

Mots clés

vérification symbolique - automates temporisés - TCTL–à la volée - DBM.

Les articles similaires

Le Chemin Oublié Comme Forme Symbolique : Analyse Sémiotique, Symbolique Et Herméneutique Du Titre Ay Abrid Ttun Medden De Lounis Aït Menguellet

Imarazene Moussa . 
pages 93-110.

Conception D’un Système Multi-agents D’aide à La Décision Pour Une Gestion Efficace Des Services D’urgence : Cas De L’hôpital De Kherrata

Boukredera Djamila .  Adel-aissanou Karima .  Abdoune Katia .  Bouriahi Lamia . 
pages 85-102.

L’utilisation Attractive Et Efficace Du Manuel Scolaire à L’ère Des évolutions Technologiques : Quelle Stratégie Pour Quelles Finalités ?

Mouri Fatima Zahra .  Oudjedi Damerdji Aouicha . 
pages 111-119.

Pour Une Gestion Efficace De L’affluence Dans Les Espaces Commerciaux

Boudriche Zohra . 
pages 22-33.

La Carte Cognitive : Un Diagramme Efficace En Classe De Fle

Gherbaoui Amar . 
pages 309-320.

Formats de citation