IMPLEMENTATION OF CONTROL SYSTEMS USING B ACTION SYSTEMS: A CASE STUDY

摘要

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.