Software Component Design with the B Method — A Formalization in Isabelle/HOL

David Déharbe 1 Stephan Merz 2, 3, *
* Auteur correspondant
2 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
3 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : This paper presents a formal development of an Isabelle/HOL theory for the behavioral aspects of artifacts produced in the design of software components with the B method. We first provide a formaliza-tion of semantic objects such as labelled transition systems and notions of behavior and simulation. We define an interpretation of the B method using such concepts. We also address the issue of component composition in the B method.
Type de document :
Communication dans un congrès
Christiano Braga and Peter Csaba Ölveczky. Formal Aspects of Component Software - 12th International Conference, FACS 2015, Oct 2015, Niterói, Brazil. Springer, 9539, pp.31-47, 2016, 〈10.1007/978-3-319-28934-2_2〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01305026
Contributeur : Stephan Merz <>
Soumis le : mercredi 20 avril 2016 - 15:40:50
Dernière modification le : mercredi 8 novembre 2017 - 12:08:08
Document(s) archivé(s) le : mardi 15 novembre 2016 - 07:51:45

Fichier

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

Identifiants

Collections

Citation

David Déharbe, Stephan Merz. Software Component Design with the B Method — A Formalization in Isabelle/HOL. Christiano Braga and Peter Csaba Ölveczky. Formal Aspects of Component Software - 12th International Conference, FACS 2015, Oct 2015, Niterói, Brazil. Springer, 9539, pp.31-47, 2016, 〈10.1007/978-3-319-28934-2_2〉. 〈hal-01305026〉

Partager

Métriques

Consultations de
la notice

207

Téléchargements du document

39