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

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.
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

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⟩

Share

Metrics

Record views

63