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

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

132