Skip to Main content Skip to Navigation
Reports

Logiques temporelles basées sur actions pour la vérification des systèmes asynchrones

Radu Mateescu 1
1 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Résumé : La vérification formelle est indispensable pour assurer la fiabilité des applications complexes et critiques comme les protocoles de télécommunication et les systèmes répartis. L'approche basée sur les modèles (model checking) consiste à traduire l'application vers un modèle système de transitions étiquetées, sur lequel les propriétés de bon fonctionnement, exprimées comme formules de logique temporelle, sont vérifiées au moyen d'algorithmes spécifiques. Ce rapport présente de manière unifiée les logiques temporelles basées sur actions qui sont actuellement les plus utilisées dans le contexte des systèmes parallèles asynchrones comportant du non-déterminisme. Les différentes logiques traitées (modales, arborescentes, régulières et de point fixe) sont illustrées à travers des exemples de propriétés typiques des systèmes parallèles asynchrones (sûreté, vivacité, équité) et sont comparées suivant l'expressivité, la facilité d'utilisation et l'efficacité des algorithmes de vérification associés.
Document type :
Reports
Complete list of metadata

Cited literature [54 references]  Display  Hide  Download

https://hal.inria.fr/inria-00071552
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 5:56:16 PM
Last modification on : Thursday, November 19, 2020 - 1:00:27 PM
Long-term archiving on: : Sunday, April 4, 2010 - 10:24:44 PM

Identifiers

  • HAL Id : inria-00071552, version 1

Collections

Citation

Radu Mateescu. Logiques temporelles basées sur actions pour la vérification des systèmes asynchrones. RR-5032, INRIA. 2003. ⟨inria-00071552⟩

Share

Metrics

Record views

245

Files downloads

748