Several tools exist providing support for model-based design of supervisors in high-tech and cyber-physical systems. On the one hand, specifically tools based on finite automata are of interest as they allow to synthesize correct supervisors from which implementations can be generated. To cope with synthesis complexity, various decentralized synthesis techniques have been proposed. In recent years, extensions were defined to deal with automata and requirements in which variables may be used. On the other hand, as the synthesis result depends on the validity of the models used as its input, other model-based techniques such as simulation, testing, and verification provide complementary support in the design process. This is especially meaningful when dealing with synthesis of supervisors for large systems. In this paper, the design process is discussed with a focus on modeling, simulation, and synthesis. Additionally, the functionalities of the available synthesis tools are presented in relation to this process. To explain models relevant in this context, a container terminal scale system is used as a case study. This system consists of 35 components (mostly sensors and actuators) and 35 requirements. The design process is evaluated and missing functionality is identified.
- continuous-time systems
- formal methods
- Model-based systems engineering
- supervisory control
- discrete-event and continuous-time systems