A Formal Approach for the Development of Automated Systems

Olfa Mosbahi 1 Leila Jemni 2 Jacques Jaray 1
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
2 MOSIC - modélisation et simulation des systèmes informatiques critiques
Abstract : This paper deals with the use of two verification approaches : theorem proving and model checking. We focus on the event B method by using its associated theorem proving tool (Click n Prove), and on the language TLA+ by using its model checker TLC. By considering the limitation of the event B method to invariance properties, we propose to apply the language TLA+ to verify liveness properties on a software behavior. We extend first of all the expressivity of a B model (called temporal B model) to deal with the specification of fairness and eventuality properties. Second, we give transformation rules from a temporal B model into a TLA+ module. We present in particular, our prototype system called B2TLA+, that we have developed to support this transformation. Finally, we verify these properties thanks to the TLC model checker.
Keywords : Automated systems Event B method Refinement Language TLA+ Liveness properties Verification
Type de document :
Communication dans un congrès
Joaquim Filipe and Boris Shishkov and Markus Helfert. 2nd International Conference on Software and Data Technologies - ICSOFT 2007, Jul 2007, Barcelone, Spain. INSTICC Press, pp.304-310, 2007
Liste complète des métadonnées

Littérature citée [6 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/inria-00158908
Contributeur : Olfa Mosbahi <>
Soumis le : lundi 2 juillet 2007 - 00:22:46
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52
Document(s) archivé(s) le : lundi 24 septembre 2012 - 10:47:01

Fichier

paper_382.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00158908, version 1

Collections

INRIA | TDS-MACS | LORIA | UNIV-LORRAINE

Citation

Olfa Mosbahi, Leila Jemni, Jacques Jaray. A Formal Approach for the Development of Automated Systems. Joaquim Filipe and Boris Shishkov and Markus Helfert. 2nd International Conference on Software and Data Technologies - ICSOFT 2007, Jul 2007, Barcelone, Spain. INSTICC Press, pp.304-310, 2007. 〈inria-00158908〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

314

Téléchargements de fichiers

113

Contact


archive-ouverte@inria.fr