ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique
Auteurs : soumettez
votre article en ligne
Autres revues >>

Technique et Science Informatiques

0752-4072
Revue des sciences et technologies de l'information
 

 ARTICLE VOL 22/4 - 2003  - pp.461-495  - doi:10.3166/tsi.22.461-495
TITRE
Logiques temporelles basées sur actions pour la vérification des systèmes asynchrones

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.

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.

AUTEUR(S)
Radu MATEESCU

Reçu le 2 septembre 2002.    Accepté le 13 mars 2003.

MOTS-CLÉS
bisimulation, logique temporelle, non-déterminisme, programme parallèle, système de transitions étiquetées, spécification, vérification.

KEYWORDS
bisimulation, temporal logic, nondeterminism, parallel program, labelled transition system, specification, verification.

LANGUE DE L'ARTICLE
Français

 PRIX
• Abonné (hors accès direct) : 12.5 €
• Non abonné : 25.0 €
|
|
--> Tous les articles sont dans un format PDF protégé par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (284 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

CONTACTS
Comité de
rédaction
Conditions
générales de vente

 English version >> 
Lavoisier