HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Spécification et vérification des propriétés de vivacité en B événementiel

Olfa Mosbahi 1 Jacques Jaray 1 Samir Ben Ahmed 2
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Résumé : Dans ce papier, nous nous intéressons à la vérification de propriétés de vivacité sur des systèmes réactifs. Nous nous basons sur le B événementiel pour la spécification et la validation de tels systèmes. En considérant la limitation du B aux propriétés d'invariance, nous proposons d'appliquer le langage TLA+ pour la vérification de telles propriétés. 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+, nous pouvons vérifier ces propriétés grâce au prouveur de théorèmes Isabelle.
Complete list of metadata

Cited literature [4 references]  Display  Hide  Download

https://hal.inria.fr/inria-00172417
Contributor : Olfa Mosbahi Connect in order to contact the contributor
Submitted on : Monday, September 17, 2007 - 10:13:34 AM
Last modification on : Friday, February 4, 2022 - 3:31:59 AM
Long-term archiving on: : Monday, September 24, 2012 - 12:26:17 PM

File

MSR2007.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00172417, version 1

Collections

Citation

Olfa Mosbahi, Jacques Jaray, Samir Ben Ahmed. Spécification et vérification des propriétés de vivacité en B événementiel. 6ème Colloque Francophone sur la Modélisation des Systèmes Réactifs - MSR 2007, Oct 2007, Lyon, France. 16 p. ⟨inria-00172417⟩

Share

Metrics

Record views

97

Files downloads

609