Formal development method of control systems using the event-based B approach Case study: A parcel sorting device

摘要

This paper presents a formal method for the development of control systems. We aim at developing a program controlling the operative part of a control system. We first build an abstract model of the operative part and complete this model to get a model of the control system. The elements introduced to change the abstract model of the operative part to the automated system forms the controller of the automated system. The next steps consists in refining the abstract model to get a model of the operative part capturing every important feature. The method is developped through a case study: a parcel sorting system.