Synthesis-Based Engineering course
With this course you can learn about Synthesis-Based Engineering (SBE). SBE is an engineering approach for the correct-by-construction development of supervisory controllers for cyber-physical systems. The approach combines model-based engineering with computer-aided design.
The course is written for engineers, students and whomever else is interested in improving their knowledge on supervisory controller development. The course explains the development of a proper supervisory controller using SBE, in a general way. This allows the knowledge that is gained during the course to be widely applied, in a variety of application domains, from health care to robotics, and infrastructure to warehousing. The course is therefore also suited for people with different backgrounds.
If you want to follow this course, it is useful to have knowledge in a technical field, such as computer science, mechanical engineering or electrical engineering. In any regard, you are expected to be capable of abstract thinking and to have some experience in problem solving. Knowledge of control systems in general, and specifically the behavior of water locks and production systems, will come in handy, but is not required. Modeling and programming skills will come in handy as well, but are also not required.
During the course, you will learn about supervisory control theory, discrete-event systems and hybrid systems. You will also make use of the CIF tools, that are part of the Eclipse ESCET™ toolkit (Eclipse Supervisory Control Engineering Toolkit). Using these tools, you will apply the theory in practice, to model and synthesize proper supervisory controllers. You will thus not only learn theory, but will also get experience in working with these tools.
The course is divided into 5 modules with different topics, and takes about 20 hours to complete. Through the various modules, you will familiarize yourself with the complete SBE development process to develop supervisory controllers. Besides synthesizing supervisory controllers, you will for instance also learn how to validate them.
During the course you will work on a water lock case, to practice what you have learned.
Learning goals
At the end of the course, after thoroughly studying the course modules and making all the assignments, you will know and understand various concepts that are essential to SBE. You will then also have gained practical experience in developing supervisory controller using SBE, and the CIF language and tools of the ESCET toolkit. Do not worry if you do not understand all of these terms yet, as you'll learn about them during the course. If you already know and are already able to do all of the following, then this course may not be for you:
- Know and understand discrete event systems theory, including what a discrete event system is, what the properties of such systems are, and what their abstraction levels are.
- Know the definition of automata with associated terms, such as locations, states, events, transitions, variables, initialization and marking.
- Be able to apply the synchronous composition of automata.
- Know concepts encountered in supervisory control synthesis, such as plants, requirements, controllable and uncontrollable events, safety, non-blockingness, controllability, and maximal permissiveness.
- Know the basic supervisory control problem and be able to apply the synthesis procedure manually on a simple uncontrolled system to gain a supervisory controller.
- Know how automata and invariants can be used to specify requirements.
- Be able to think in restrictions imposed by requirements on the behavior of the uncontrolled system.
- Have a basic understanding of the CIF language, to be able to use CIF to make a model of the uncontrolled system and the requirements.
- Be able to use the CIF tools to synthesize a supervisory controller.
- Be able to use the CIF tools for simulation to validate the synthesized controller.
- Gained practical experience by developing a controller for a water lock.
Learning materials
For this course, you will make use of some course files. These course files are bundled with the ESCET toolkit that is used during the course. There is no need to install the toolkit before you start the course, since you will get instructions on how to download and install it during the course. You will then also find out how to get the course files.
Course setup
The course consists of 5 modules. Each module starts by multiple sub-modules that explain the theory. At the end of most sub-modules, you can test your understanding of the theory using a small quiz or some small exercises. Besides theory, there are also sub-modules that explains how the theory can be applied using CIF. Near the end of each module, there is a sub-module with more challenging exercises. These exercises require a deeper understanding of the theory, to be able to correctly apply the theory in practice. Throughout the course, you will work on developing a supervisory controller for a water lock. The water lock is a larger case. In each module you will construct a part of it, in a step-by-step fashion through various assignments. At the end of each module, you will thus directly apply what you have learned to this case.
The time required to follow the course is roughly 20 hours in total, 4 hours per modules. For each module, learning the new theory and how to apply it takes about 1.5 hours. The exercises near the end of each module and the assignments to work on the water lock case take about 2.5 hours per module.
It is recommended to follow one module of the course per day (4 hours a day). The full course can then be completed in 5 days.
Course modules
Module 1: Supervisory control of discrete event systems
In this module you are introduced to supervisory controllers for cyber-physical systems. You learn about the different engineering approaches for supervisory controllers, including synthesis-based engineering, and their advantages and disadvantages. One of the first challenges in engineering such systems is how to capture their behavior. You will learn how to express their behavior in models, that can be understood and reasoned about unambiguously. Especially for larger systems, and if multiple people studying a system's behavior, it is very useful if they all understand it in the same way. In this module, we will introduce discrete event systems modeled as automata, for that. You get started with using the Eclipse ESCET toolkit and the CIF tools, will make your first CIF models consisting of automata, and simulate them to understand their behavior. You are also introduced to the water lock case.
Module 2: Working with automata
In this module, you dive deeper into the concepts related to automata, and you will learn more about using multiple automata that interact. You learn about terms like reachability, deadlock, non-determinism and synchronization. You extend your knowledge of modeling automata with CIF, and learn new ways of using variables. And you will work with more CIF tools.
Module 3: Supervisory control and plant models
In this module, you will dive deeper into supervisory control theory and supervisory controller synthesis. You learn among others the difference between controllable and uncontrollable events, and some of the properties that a proper supervisors adheres to, namely that it is safe, controllable, non-blocking and maximally permissive. You apply these concepts to simple problems. You expand your knowledge and experience in modeling plant models using CIF. You apply it to model the plants of the water lock case.
Module 4: Modeling requirements and supervisor synthesis
In this module, you will learn about user-specified requirements, that indicate what undesired or unsafe situations must never occur. You will learn about the different types of user-specified requirements, their pros and cons, and how to model them in CIF. You will also learn about how synthesis ensures that the controlled system adheres to the specified requirements. And, you will synthesize your first supervisory controller. You put all this in practice, by modeling the requirements for the water lock case and synthesizing a supervisor for it.
Module 5: Hybrid simulation models
In this module, you learn the concepts of timed and hybrid systems, and how to model them in CIF. You extend discrete event models with continuous behavior, to create a hybrid model for the water lock case. You use the improved simulation model to validate the final supervisory controller, making sure it operates as intended.