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

David Déharbe and Stephan Merz

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 formalization 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.

© Springer 2015

Available as: PDF | Isabelle theories

Reference

@InProceedings{deharbe:b-component,
  author =       {David D{\'e}harbe and Stephan Merz},
  title =        {Software component design with the {B} method -- a formalization in {Isabelle/HOL}},
  booktitle =    {Intl. Conf. Formal Aspects of Component Software},
  publisher = {Springer},
  year =      2015,
  editor =    {Christiano Braga and Peter Csaba Ölveczky},
  series =    {LNCS},
  volume =    9539,
  pages =     {31-47},
}