Verification and validation
After applying supervisor synthesis it is time to analyze the resulting supervisor model, using verification and validation, and adapt the plants and requirements if any issues are found.
Verification
Verification to ensure that the synthesized supervisor satisfies the requirements that were used for synthesis is superfluous, as the synthesized model is correct-by-construction. However, verification may still be needed for additional requirements that are not yet supported by synthesis, such as stronger liveness requirements and timed requirements.
The synthesized supervisor model should be checked for various properties using the controller properties checker tool. Further verification may be performed by transforming the supervisor model to formats of external verification tools, such as mCRL2 and UPPAAL, and then using such tools to perform the actual verification.
Validation
Furthermore, the supervisor should be validated to ensure it behaves as intended. The specified requirements could not be the desired requirements, as they could for instance be wrongly specified or too strict, resulting in the system being controlled by the controller exhibiting unwanted or insufficient behavior.
The CIF simulator can be used to simulate CIF specifications. Especially when combining this with SVG visualization and interactive simulation, it is a very powerful way to validate whether the supervisory controller controls the system as intended. This may for instance reveal that additional requirements are needed, or existing requirements need to be adapted.
Next steps
In case issues are found through verification or validation, these need to be addressed. Typically this involves changes to either the plant model or requirements model. After such changes, the supervisor can be re-synthesized automatically. Changes can be made iteratively, until confidence in the correctness of the controller is high enough.
The next step in the process to apply synthesis-based engineering in practice is then to implement the supervisory controller.