Developing control systems with some fragile environment

Event-B is a formal method that allows one to model various kinds of systems including control systems working within some fragile environment. However, it is lacking a systematic approach for developing this type of systems and it hinders the applicability of Event-B. Our contribution is such an approach and it is presented in this paper. Our proposed method focuses on a set of elements that should be captured by the formal model and prescribes an order in which they should be introduced. The key aspect of our approach is to first model the required behaviour of the environment, and then to introduce the controller to appropriately influence the environment. It has the advantage that every step of the such a development is dictated by the information available so far, including the requirements. We argue that having a clear development strategy early in the design process will assist the developers in producing high-quality models of the future software systems