Skip to Main content Skip to Navigation
New interface
Conference papers

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
MPII - Max-Planck-Institut für Informatik, 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.
Document type :
Conference papers
Complete list of metadata
Contributor : Stephan Merz Connect in order to contact the contributor
Submitted on : Wednesday, April 20, 2016 - 3:40:50 PM
Last modification on : Thursday, January 20, 2022 - 5:26:13 PM
Long-term archiving on: : Tuesday, November 15, 2016 - 7:51:45 AM


Files produced by the author(s)




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⟩



Record views


Files downloads