Skip to Main content Skip to Navigation
Conference papers

Utilisation conjointe de B et TLA+ pour la modélisation et la vérification des systèmes réactifs

Olfa Mosbahi 1, 2 Leila Jemni Ben Ayed 1
1 FST - Faculté des Sciences Mathématiques, Physiques et Naturelles de Tunis
2 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Résumé : La méthode B fournit un cadre rigoureux de développement de systèmes mais sa limitation concerne le type des propriétés exprimées car seuls les invariants sont considérés. Notre travail a pour objectif d'utiliser le B événementiel pour exprimer des propriétés temporelles de fatalité et d'équité. La logique temporelle des actions TLA+ a prouvé son efficacité dans l'expression et la vérification de propriétés d'équité. Elle se base sur le concept de raffinement, d'action et de transition qui exprime une compatibilité avec une modélisation B événementiel. Notre contribution consiste à proposer une méthode de spécification et de vérification utilisant conjointement B et TLA+ et leur outils de vérification l'AtelierB et le prouveur de théorèmes Isabelle.
Mots-clés : Modélisation Preuve Propriétés d'équité Propriété de fatalité Méthode B Raffinement Systèmes réactifs Vérification
Document type :
Conference papers
Complete list of metadata
https://hal.inria.fr/inria-00000800
Contributor : Mohamed Khalgui <>
Submitted on : Sunday, November 20, 2005 - 10:46:20 AM
Last modification on : Friday, February 26, 2021 - 3:28:04 PM

Identifiers

  • HAL Id : inria-00000800, version 1

Collections

CNRS | INRIA | LORIA | UNIV-LORRAINE

Citation

Olfa Mosbahi, Leila Jemni Ben Ayed. Utilisation conjointe de B et TLA+ pour la modélisation et la vérification des systèmes réactifs. Premières Rencontres des Jeunes Chercheurs en Informatique Temps Réel 2005 - RJCITR'05, Sep 2005, Nancy, France. pp.31-34. ⟨inria-00000800⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

132

 

Contact                    Legal Notice                    Personal Data