High-tech companies increasingly adopt the Model-Based Systems Engineering (MBSE) paradigm. The use of (formal) models for controller design allows validation and verification of controllers long before they are implemented and integrated into the system. Early validation and verification have been shown to lead to less defects and reduced costs.
The Eclipse Supervisory Control Toolkit (ESCT) project provides a toolkit for the development of supervisory controllers in the MBSE paradigm. The toolkit has a strong focus on model-based design, supervisory controller synthesis, and industrial applicability, for example to cyber physical systems. The toolkit supports the entire development process of (supervisory) controllers, from modeling, supervisory controller synthesis, simulation-based validation and visualization, and formal verification, to real-time testing and implementation.
Supervisory controller synthesis is the key feature of the toolkit. It involves the automatic generation of supervisory controllers from a specification of the uncontrolled system and the (safety) requirements that the controller needs to enforce. This shifts controller design from ‘how should the implementation work’ to ‘what should the controller do’. Implementation of the controller is achieved through (implementation language) code generation, reducing the number of errors introduced at this stage.
The ESCT project currently features one modeling language, CIF. The language is a powerful automata-based modeling language for the specification of discrete event, timed (linear dynamics), hybrid (piecewise continuous dynamics) systems. It can be seen as a rich state machine language with the following main features:
- Modular specification with synchronized events and communication between automata.
- Many data types are available (booleans, integers, reals, tuples, lists, arrays, sets, and dictionaries), combined with a powerful expression language for compact variables updates.
- Text-based specification of the automata, with many features to simplify modeling large non-trivial industrial systems.
- Primitives for supervisory controller synthesis are integrated in the language.
Highlights of the CIF tooling in the ESCT project:
- Text-based editor that allows to easily specify and edit models.
- Feature-rich powerful data-based synthesis tool. A transformation to the supervisory controller synthesis tool Supremica is also available.
- A simulator that supports both interactive and automated validation of specifications. Powerful visualization features allow for interactive visualization-based validation.
- Conversion to formal verification tools such as mCRL2 and UPPAAL.
- Implementation language code generation (PLC languages, Java, C, and Simulink) for real-time testing and implementation of the designed controller.