Vérification des propriétés temporelles des programmes parallèles

Radu Mateescu

PhD thesis, Institut National Polytechnique de Grenoble, April 1998.

Abstract:

Formal verification is essential in order to ensure reliability of critical applications like communication protocols and distributed systems. The so-called model-checking verification technique consists in translating the application into a Labelled Transition System (LTS) on which the desired properties, expressed in temporal logic, are verified using specialized tools called model-checkers. However, the "classical" temporal logics, defined over an alphabet of atomic actions, are not well-adapted for description languages as LOTOS, whose actions contain typed values.

This thesis defines a formalism called XTL (eXecutable Temporal Language), which allows to express temporal properties involving the data handled by the program to be verified. XTL is based upon an extension of the modal mu-calculus with typed variables. The values contained in the LTS, extracted using extended modal operators, can be passed as arguments to the fixed point operators or can be combined by means of functional-like constructs as "let", "if-then-else", "case", etc. The properties over action sequences of the program can be described succinctly using regular expressions. Special meta-operators allow to evaluate formulas on an LTS as well as to express non-standard temporal properties by exploring the transition relation.

The semantics of XTL is formally defined, and efficient algorithms are proposed for the evaluation of temporal XTL formulas over LTS models. A model-checker for XTL is developed and successfully used for the validation of industrial applications such as the BRP protocol designed by Philips and the link layer of the IEEE-1394 serial bus ("FireWire").

Keywords:

labelled transition system, LOTOS, mu-calculus, specification, temporal logic, validation, verification.

Résumé :

La vérification formelle est indispensable pour assurer la fiabilité des applications critiques comme les protocoles de communication et les systèmes répartis. La technique de vérification basée sur les modèles (model-checking) consiste à traduire l'application vers un système de transitions étiquetées (STE), sur lequel les propriétés attendues, exprimées en logique temporelle, sont vérifiées à l'aide d'outils appelés évaluateurs (model-checkers). Cependant, les logiques temporelles "classiques", définies sur un vocabulaire d'actions atomiques, ne sont pas adaptées aux langages de description comme LOTOS, dont les actions contiennent des valeurs typées.

Cette thèse définit un formalisme appelé XTL (eXecutable Temporal Language) qui permet d'exprimer des propriétés temporelles portant sur les données du programme à vérifier. XTL est basé sur une extension du mu-calcul modal avec des variables typées. Les valeurs contenues dans le STE, extraites à l'aide d'opérateurs modaux étendus, peuvent être passées en paramètre aux opérateurs de point fixe ou manipulées à l'aide de constructions d'inspiration fonctionnelle comme "let", "if-then-else", "case", etc. Les propriétés portant sur des séquences d'actions du programme sont décrites succinctement au moyen d'expressions régulières. Des méta-opérateurs spéciaux permettent l'évaluation des formules sur un STE et l'expression de propriétés temporelles non-standard par exploration de la relation de transition.

La sémantique de XTL est formellement définie et des algorithmes efficaces sont proposés pour évaluer des formules temporelles XTL sur des modèles STEs. Un évaluateur XTL est développé et utilisé avec succès pour la validation d'applications industrielles comme le protocole BRP développé par Philips et la couche liaison du bus série IEEE-1394 ("FireWire").

Mots-clés :

logique temporelle, LOTOS, mu-calcul, spécification, système de transitions étiquetées, validation, vérification.

274 pages

PDF

PostScript