Where academic tradition
meets the exciting future

Implementation of Control Systems using B Action Systems: A Case Study

Pontus Boström, Marina Waldén, Implementation of Control Systems using B Action Systems: A Case Study. Nordic Journal of Computing 11(2), 75–101, 2004.

Abstract:

In this paper we present a methodology for implementing reactive control
systems of industrial size using formal methods. The methodology is
applied in a case study from the healthcare technology field. We use
B Action Systems as our theoretical framework for developing reliable
and correct control systems in a stepwise manner. For proving the
correctness of each development step we rely on the tool support provided
for the B Method. With the tool the formally developed system can
be translated to a programming language. Hence, the implementation
method provides a precise mapping from the specification to the code
executed on the computer. This is needed especially in industry for
developing large correct systems. In the case study we develop software
for part of a microplate liquid handling workstation. The design
methodology has previously been used for specifying control systems of
industrial size, but here we extend the methodology to also consider code
generation issues for such systems.

BibTeX entry:

@ARTICLE{jBoWa04a,
  title = {Implementation of Control Systems using B Action Systems: A Case Study},
  author = {Boström, Pontus and Waldén, Marina},
  journal = {Nordic Journal of Computing},
  volume = {11},
  number = {2},
  pages = {75–101},
  year = {2004},
  keywords = {B Method, Action Systems, discrete control systems, stepwise refinement, implementation, industrial applications},
}

Belongs to TUCS Research Unit(s): Distributed Systems Laboratory (DS Lab)

Publication Forum rating of this publication: level 1

Edit publication