Currently automatic control deals with the theoretical modelling techniques applied to formally define the behaviour of a control system when the system goals and the process behaviour to be controlled are well defined. Although these approaches are efficient in the design and implementation phases for controlling the dynamics of automatized systems, other tools are also required in the early stages of the process of engineering a system. This paper deals with a specification method aimed at proving that the system goals, as required by the users, are formally refined towards the real target automation system with completeness, consistency, unambiguousness and correctness guarantees. Our specification method is based on the B language to globally verify, from formal constructs, the predicate: Control Systems Requirements ⋀ Process Systems Requirements ⇒ Production System Requirements. A case study illustrates our approach and opens issues on the way to industrial practice.Currently automatic control deals with the theoretical modelling techniques applied to formally define the behaviour of a control system when the system goals and the process behaviour to be controlled are well defined. Although these approaches are efficient in the design and implementation phases for controlling the dynamics of automatized systems, other tools are also required in the early stages of the process of engineering a system. This paper deals with a specification method, based on the B language, that aims at proving that the system goals, as required by the users, are formally refined towards the real target automation system with completeness, consistency, unambiguousness and correctness guarantees. A case study illustrates our approach and opens issues on the way to industrial practice.
