Software component design with the B method — a formalization in Isabelle/HOL?

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. Key words: B-method, formal semantics, Isabelle/HOL, simulation