thesis

Reformulation et vérification de propriétés temporelles dans le cadre du raffinement de systèmes d'évènements

Defense date:

Jan. 1, 2002

Edit

Institution:

Besançon

Disciplines:

Computer sciences

Authors:

Directors:

Abstract EN:

We are interested in verifying temporal properties in event systems specified by refinement. We adopt a four-step method : 1- We verify an abstract property by model-checking; 2- We refine the system and verify the refinement; 3- We refine the abstract property into a reformulated property; 4- We verify the reformulated property; The main interest is in one hand to have the abstract properties refined by the specifier to take into account the details introduced during refinement, on the other hand to decrease the verification effort by combining proof and model-checking. This work, based on a refinement definition between labelled Kripke structures lead us to prove the preservation of PLTL properties through refinement and the correctness of the verification method for a set of reformulation patterns. This work is implemented in a prototype using the PVS prover.

Abstract FR:

Les travaux présentés se placent dans le contexte de la vérification de propriétés temporelles sur des systèmes d'événements spécifiés par raffinement. Notre démarche se décompose en quatre étapes : 1-Nous vérifions une propriété abstraite par model-checking; 2- Nous raffinons le système et vérifions ce raffinement ; 3- Nous raffinons la propriété abstraite en une propriété dite reformulée; 4- Nous vérifions la propriété reformulée. L'apport de ces travaux est d'une part de permettre à l'utilisateur de raffiner les propriétés pour tenir compte des détails introduits lors du raffinement, d'autre part de diminuer l'effort de vérification en combinant preuve et model-checking. Ce travail, basé sur une définition de raffinement entre structures de Kripke étiquetées, nous a conduit a prouver la préservation des propriétés PLTL par raffinement et la correction de la démarche de vérification pour un ensemble de schémas de reformulation. Notre technique est implantée dans un prototype utilisant le prouveur PVS.