Extended Liveness Capabilities for Synthesis in CIF - A Rijkswaterstaat case study

Synthesis based engineering (SBE) is an approach in which supervisor synthesis is utilized to automatically generate a correct-by-construction supervisor for a cyber-physical system. The Eclipse Supervisory Control Engineering Toolkit (ESCET—) project develops a state-of-the-art toolkit supporting the entire SBE workflow mainly through the CIF language and tools. Rijkswaterstaat (RWS) utilizes SBE and CIF to develop supervisors for complex systems such as waterway locks. However, RWS encountered a challenge during experimentation with requirement state invariants. After the addition of such an invariant, the synthesized supervisor did not allow a waterway lock gate to be opened or closed from certain reachable states in the controlled system. The standard liveness constructs of CIF proved insufficient to guarantee the ability to open and close a lock gate from all reachable states. The absence of such guarantees motivated the work of this thesis to extend CIF with additional liveness capabilities. We researched the state of the art in supervisory control theory regarding liveness requirements in a literature study and formulated two possible approaches to guarantee the reachability of multiple desired states: an algorithmic approach adapting the synthesis algorithm to incorporate the desired liveness requirements, and a novel model-based approach utilizing existing CIF constructs and classical Ramadge and Wonham (RW) supervisory control theory to express the desired liveness requirements. Due to the novelty of the model-based approach, we proved its correctness using the RW-framework in the context of CIF. Lastly, we compared both approaches experimentally on a set of 15 benchmark models which either directly model real cyber-physical systems or are inspired by them. The experiments clearly show the superiority of the algorithmic approach over the modelbased approach as it is on average 7.6 times faster and uses 1.2 times less memory. Therefore, the algorithmic approach has been adopted in CIF v10.0 to support liveness requirements semantically expressing CTL formula AG EF ϕ, where ϕ is a predicate capturing desired states. This feature solves the challenge faced by RWS and strengthens the correct-by-construction notion of synthesis by providing more precise conditions under which a supervisor is considered correct.