Un Vérificateur Symbolique Efficace
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:
Publié dans la revue: Synthèse
Nos services universitaires et académiques
Thèses-Algérie vous propose ses divers services d’édition: mise en page, révision, correction, traduction, analyse du plagiat, ainsi que la réalisation des supports graphiques et de présentation (Slideshows).
Obtenez dès à présent et en toute facilité votre devis gratuit et une estimation de la durée de réalisation et bénéficiez d'une qualité de travail irréprochable et d'un temps de livraison imbattable!
Aucun fichier associé
Si le fichier est volumineux, l'affichage peut échouer. Vous pouvez obtenir le fichier directement en cliquant sur le bouton "Télécharger".
