B événementiel et les propriétés de vivacité

Olfa Mosbahi 1 Jacques Jaray 1
1 MOSEL - Proof-oriented development of computer-based systems
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Résumé : 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.
Type de document :
Article dans une revue
Journal Européen des Systèmes Automatisés (JESA), Lavoisier, 2010, 44 (9-10), pp.1119-1163. 〈10.3166/jesa.44.1119-1163〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00580131
Contributeur : Dominique Méry <>
Soumis le : samedi 26 mars 2011 - 11:07:34
Dernière modification le : mardi 24 avril 2018 - 13:53:16

Identifiants

Collections

Citation

Olfa Mosbahi, Jacques Jaray. B événementiel et les propriétés de vivacité. Journal Européen des Systèmes Automatisés (JESA), Lavoisier, 2010, 44 (9-10), pp.1119-1163. 〈10.3166/jesa.44.1119-1163〉. 〈inria-00580131〉

Partager

Métriques

Consultations de la notice

86