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 <>
Submitted on : Monday, September 17, 2007 - 10:13:34 AM
Last modification on : Friday, February 26, 2021 - 3:28:05 PM
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

271

Files downloads

813