A formal development approach of control systems using the event based B approach

摘要

In this paper we present a way to specify reactive systems with the event based B method. We focus on the refinement process used for the development of a control system such as when it's composed with the physical device, it forms a controlled system satisfying requirements. In this approach, we start with a model of the physical device and a model of a minimal controller. The model of the controller will be refined until desired properties are satisfied. The proposed solution is detailed through the example of a computer controlled gas burner.