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.
Type de document :
Communication dans un congrès
6ème Colloque Francophone sur la Modélisation des Systèmes Réactifs - MSR 2007, Oct 2007, Lyon, France. 16 p., 2007
Liste complète des métadonnées

Littérature citée [4 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00172417
Contributeur : Olfa Mosbahi <>
Soumis le : lundi 17 septembre 2007 - 10:13:34
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52
Document(s) archivé(s) le : lundi 24 septembre 2012 - 12:26:17

Fichier

MSR2007.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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., 2007. 〈inria-00172417〉

Partager

Métriques

Consultations de la notice

201

Téléchargements de fichiers

492