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

David Déharbe 1 Stephan Merz 2, 3, *
* Corresponding author
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
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik
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.
Document type :
Conference papers
Liste complète des métadonnées

https://hal.inria.fr/hal-01305026
Contributor : Stephan Merz <>
Submitted on : Wednesday, April 20, 2016 - 3:40:50 PM
Last modification on : Tuesday, February 19, 2019 - 3:40:03 PM
Document(s) archivé(s) le : Tuesday, November 15, 2016 - 7:51:45 AM

File

paper.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

David Déharbe, Stephan Merz. Software Component Design with the B Method — A Formalization in Isabelle/HOL. Formal Aspects of Component Software - 12th International Conference, FACS 2015, Oct 2015, Niterói, Brazil. pp.31-47, ⟨10.1007/978-3-319-28934-2_2⟩. ⟨hal-01305026⟩

Share

Metrics

Record views

334

Files downloads

205