Formal Composition Algorithm for the Synthesis of a Correct Controller Implementation

Abstract This paper presents a composition algorithm for the synthesis of a supervisory controller, starting from high-level specifications given in Grafcet. This framework considers the constraints induced by the behaviour of the controlled plant so as to identify the required correct behaviour of Grafcet during control execution.