A composition-based approach for the development of automated embedded systems

This paper deals with the use of the event B method to develop an automated system as a closed one with two components : the controller and the controlled. The first is a software component controlling the second one that models the physical device and its environment. A formal method is proposed to co-design separately these components before their composition defined with the event B method to prove thereafter the system correctness. The different aspects of our work are illustrated on the example of a parcel sorting system.