Supervisor synthesis
Having modeled the plants and requirements, the supervisory controller can automatically be synthesized. Supervisory controller synthesis (or simply supervisor synthesis) automatically generates a supervisor, from the models of the uncontrolled system (plant model) and control requirements (requirements model).
The synthesized supervisor is correct-by-construction, satisfying various properties. It is safe (satisfies all the requirements), controllable (limits only controllable events, not uncontrollable ones), is non-blocking (does not block, a form of liveness), and is maximally permissive (imposes no more restrictions than is necessary).
CIF supports supervisor synthesis through the following tools:
The data-based synthesis tool is generally more efficient and supports a larger subset of CIF language concepts. It is therefore recommended over the event-based synthesis tool.
The documentation of these tools provide further details on how to use them.
The next step in the process to apply synthesis-based engineering in practice is to perform validation.