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

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 Connect in order to contact the contributor
Submitted on : Sunday, November 20, 2005 - 10:46:20 AM
Last modification on : Friday, February 4, 2022 - 3:31:18 AM

Identifiers

  • HAL Id : inria-00000800, version 1

Collections

CNRS | INRIA | LORIA | UNIV-LORRAINE | INRIA2

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 Datacite

Share

Metrics

Record views

63

 

Contact                    Legal Notice                    Personal Data