Development of Control Systems Guided by Models of their Environment

Event-B is a formal method that allows one to develop various kinds of systems including discrete control systems. 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 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.