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

Radu Mateescu

Technique et Science Informatiques, 2003

Full version available as INRIA Research Report RR-5032.

Abstract:

Formal verification is essential for ensuring the reliability of complex, critical applications such as communication protocols and distributed systems. The model-checking approach consists in translating the application into a labelled transition system model, on which the correctness properties, expressed as temporal logic formulas, are verified by means of specific algorithms. This article presents in a unified manner the action based temporal logics that are currently the most used in the framework of parallel asynchronous systems involving nondeterminism. The different logics described (modal, branching, regular, and fixed point based) are illustrated through various examples of typical properties of parallel asynchronous systems (safety, liveness, fairness) and are compared with respect to expressiveness, user-friendliness, and efficiency of the corresponding verification algorithms.

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. Cet article 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.

39 pages

PDF

PostScript