B événementiel et les propriétés de vivacité
Résumé
This paper deals with the verification of liveness properties on reactive systems. We are based on the event B method to specify and validate such systems. By considering the limitation of the B to invariance properties, we propose to apply the language TLA+ to verify liveness properties on a software behavior. We extend, in particular, the expressivity and the semantics of the event B method to deal with the specification n of fairness and eventuality properties. By transforming an extended B model into TLA+ module by using a prototype system (B2TLA+) that we have developed, we can verify these properties thanks to the modelchecker TLC on finite state systems. For the verification of infinite-state systems, we propose the use of predicate diagrams.
Dans cet article, nous nous intéressons à la vérification de propriétés de vivacité sur des systèmes réactifs. Nous nous basons sur B événementiel pour la spécification et la validation de tels systèmes. En considérant la limitation de B aux propriétés d'invariance, nous proposons d'appliquer le langage TLA+ pour la vérification des propriétés de vivacité. Nous étendons, en particulier, l'expressivité et la sémantique d'un modèle B pour obtenir un modèle B temporel. En transformant le modèle B étendu en un module TLA+ grâce à un prototype (B2TLA+) que nous avons développé, nous pouvons vérifier ces propriétés sur des systèmes à états finis grâce au model-checker TLC. Pour la vérification de ces types de propriétés sur des systèmes à états infinis, nous utilisons les diagrammes de prédicats.