Synthesis-based engineering
Synthesis-based engineering is a form of model-based engineering. It uses supervisory controller synthesis (or simply supervisor synthesis) to automatically synthesize a correct-by-construction controller model.
Synthesis-based engineering process
The following figure shows a simplified development process for synthesis-based engineering of supervisory controllers:
As with general model-based engineering, at the center is a controller model with a mathematical foundation. From the controller model, the control software can still be manually implemented or automatically generated.
However, with synthesis-based engineering, the controller model is not manually modeled from design documents. Instead, it is automatically generated from models of the uncontrolled system (plant model) and control requirements (requirements model).
Verification to ensure that the controller (model) satisfies the requirements used for synthesis is then superfluous, as the synthesized controller model is correct-by-construction. Verification may still be needed for additional requirements that are not yet supported by synthesis, such as stronger liveness requirements and timed requirements.
Validation that the controller model behaves as intended is still needed, because even though synthesis guarantees that the synthesized controller correctly adheres to the specified requirements, the specified requirements may not be the desired requirements. For instance, the requirements could be incomplete, too restrictive, or contain other mistakes, resulting in the system being controlled by the controller exhibiting behavior that is not desired or not showing behavior that is desired.
Input: plant and requirements models
Supervisor synthesis requires two types of models as input. The first type of model is called a plant model, after the concept of plant from control theory. Plant models describe capabilities or behavior of a physical system 'as is', without any integrated control. They represent the possible behavior of the uncontrolled system. The second type of model is called a requirements model. Requirements models describe the requirements that the controller must adhere to. They model restrictions upon the behavior of the plants, to ensure that only the desired behavior remains.
A plant model can for instance specify which sensors and actuators are present in the system. It may also specify their interdependencies. For instance, a sensor that indicates that a gate is open and a sensor that indicates it is closed, can under normal circumstances not be enabled at the same time. A plant model is often modeled as a state machine. The following figure shows as an example a the combined plant model for the two gate sensors:
Initially it is closed. As the gate is opened, the gate closed sensor goes off, and the gate is somewhere in between. Then it can be closed again, making the gate closed sensor go on. But the gate can also keep going further open, until it is fully opened, and the gate open sensor goes on. There is can be closed again, making the gate open sensor go off. The plant model clearly states that it is not possible for the gate to be open and closed at the same time, as the plant model can only be in one state at a time.
Actions, such a sensor going on or off, or an actuator being turned on or off, are called events. Supervisor synthesis distinguishes two types of events, controllable and uncontrollable events. Controllable events can be controlled by the supervisory controller. Actuators are typically modelled as controllable events, such that the supervisory controller decides when to actuate them. Uncontrollable events operate autonomously, from the perspective of the supervisory controller. A controller can not prevent such events from occurring in the system. For instance, a user may push a button and the corresponding sensor will indicate whether the button is pushed or not. The events to indicate changes in the status of the sensor will happen. The supervisor can not prevent this. Another example of uncontrollable events is limit sensors of movements. When a movement is completed, its limit sensor will be activated, leading to an uncontrollable event being fired.
Plant models at the relatively low abstraction level of sensors and actuators are quite common. However, modeling and controlling (sub-)systems at a higher abstraction level is possible as well. See for more information the section on supervisory controllers.
A requirements model captures requirements. It may specify functional requirements, safety requirements, etc. For instance, the motor to open a gate may only be activated once the barrier to stop traffic is fully closed. Control requirements can also be specified as state machines, but often the use of a logical formula is more intuitive. Combining them is also possible. Well-formulated logical formulas are easy to understand, even for people without a mathematical background. As an example, consider a requirement in three forms: natural language, mathematical formula, and modeled in CIF:
Natural language: "The actuator to open the gate may only be activated if the barrier is fully closed."
Mathematical formula: gate_open_actuator.c_on ⇒ barrier_sensors.closed
Modeled in CIF as a state/event exclusion requirement:
requirement gate_open_actuator.c_on needs barrier_sensors.closed;
Supervisory controller synthesis
Supervisory controller synthesis generates from the plant and requirements models a controller model, a model of the control logic, named a supervisor or supervisory controller. The synthesized supervisor is correct-by-construction, i.e., it satisfy all the requirements in every situation.
The supervisor may be represented as another state machine, but it may for instance also be a list of conditions under which actuators may be activated or deactivated. The synthesized supervisor as a state machine, or the plant model together with the supervisor in the form of extra synthesized control conditions, forms the controlled system.
The controlled system is guaranteed to satisfy the following properties:
Safe: It satisfies all specified requirements in all situations that the specified uncontrolled system can be in.
Controllable: It only limits controllable events of the plant, e.g., it may prevent enabling or disabling an actuator, but can’t prevent a sensor from going on or off.
Maximally permissive: It does not impose more restrictions than strictly necessary to enforce the previous properties, i.e., it is maximally permissive. In other words, the controlled system permits all safe, controllable, and non-blocking behaviors, i.e., it is minimally restrictive.
In practice the terms supervisor and controller are often used interchangeably. Formally however, they can be different. A supervisor is maximally permissive and may still allow multiple (safe) choices, for instance between enabling multiple different actuators, or between enabling one actuator and disabling another one. A controller is considered to explicitly choose specific controllable events rather than allowing multiple ones.
Benefits of synthesis-based engineering
Synthesis-based engineering has all the benefits of model-based engineering. Additionally, it has the following benefits:
- Computer-aided design for improved quality at reduced effort and cost
-
Computer-aided design and automation shorten the development cycle and reduce human errors. This improves the quality and reliability of controllers, and reduces effort and costs.
More concretely, supervisor synthesis provides computer-aided design assistance. It can for instance automatically detect conflicting requirements. It will also detect that a certain activator may never be enabled in a certain state, because under certain specific conditions this may later lead to an unavoidable unsafe state. For complex systems, this kind of situations are often difficult to foresee for human beings. It is therefore difficult to correctly manually model them in a controller model.
- Focus on the what rather than the how
-
With synthesis-based engineering the controller model is automatically synthesized. From it, the implementation is automatically produced through code generation. Verification is (to a large degree) not needed as the implementation is correct-by-construction. The focus therefore shifts to requirements design and validation. Engineers can thus focus on 'what should the controller do' (its requirements), rather than on 'how must the controller achieve this' (the controller design and implementation).
An example is specifying a First-In-First-Out (FIFO) requirement. While specifying it may be quite easy, realizing the requirement in a controller model may be complex due to the various situations that may arise in the system. Supervisory controller synthesis can evaluate all possible combinations of conditions and synthesize a controller that is mathematically correct for all of them. This kind of design automation is even more useful when multiple, complex and related requirements need to be considered. The synthesized supervisor is correct-by-construction for all requirements in all situations, preventing human errors.
- Verification exposes problems, synthesis solves them
-
Synthesis-based engineering goes far beyond verification-based engineering. Formal verification exposes problems. It tells you that the controller model is not correct and in which situations, and you need to iteratively adapt it yourself. Each time formal verification produces a counter example to indicate a requirement violation, the controller model needs to be manually adapted. Contrary, supervisor synthesis provides solutions. It automatically synthesizes a controller model that satisfies all the requirements. Synthesis produces in one go a supervisor with all the additional conditions that must be enforced to ensure all requirements are satisfied. This makes verification of the controller model against the requirements from which the supervisor was synthesized superfluous, as the synthesized controller model is already correct-by-construction.
- Maintain maximum design space freedom
-
Maximal permissiveness ensures that maximum design space freedom is maintained. When manually designing a controller, an engineer may favor simple control conditions that severely limit the design space. As synthesis produces maximally-permissive supervisors, it imposes minimal restrictions, while still satisfying all requirements. This leaves design space freedom to e.g. choose performance-optimal solution among safe alternatives. A performance-optimal controller may for instance be derived from a supervisor model that allows multiple (safe) choices.
- Supports a comprehensive modular design and efficient incremental engineering
-
Each part of the plant and each requirement can be specified separately. This way it is easy to adapt specific plants or requirements, or add new ones. Modular specifications thus allow for efficient incremental engineering, as after each change a simple re-synthesis is enough to obtain a new correct-by-construction controller.
- Supports reuse and standardization
-
The separately specified plants and requirements can even be put in libraries with reusable standardized building blocks. This allows engineers to easily build up new specifications from existing proven building blocks, combining them in different ways. Ultimately this leads to more uniformity and improves efficiency.
- Intuitive specifications with fine-grained requirement traceability
-
Each plant and requirement can be specified separately, and has a clear purpose. This provides a good overview of the control requirements, and allows for fine-grained requirement traceability. This unlike the controller model itself. There, one requirement can have an effect on various parts (states) of the controller. It can thus be spread out over the controller model, and mixed with other requirements. Clear modular specifications avoid hiding undesired and unneeded behavior in a large/complex controller.
See the synthesis-based engineering example section for a concrete example that shows the power of synthesis.
Even though synthesis-based engineering has many benefits, companies should not underestimate how significantly different it is from traditional engineering or even from lesser-automated forms of model-based engineering, such as verification-based engineering. They should consider and manage the challenges particular to this engineering approach.
Terminology
The following terminology is often used when discussing synthesis-based engineering of supervisory controllers, in additional to model-based engineering terminology:
- Controllable event
-
An event that is controlled (enabled or disabled) by the controller. Events to actuate (turn on or off) an actuator are often controllable events.
- Controlled system
-
The uncontrolled system together with a supervisor or controller that controls it. This may be represented as a single state machine, or as a combination of the _plant model with the supervisor or controller model.
- Controller
-
A controller model that explicitly chooses specific controllable events, rather than allowing multiple ones as a supervisor may do. When this distinction is not relevant, supervisor and controller are often used interchangeably.
- Correct-by-construction formal method
-
A formal method that guarantees that the result of the method satisfies all requirements.
- Event
-
An action representing something that can happen in the system. For instance, there may be low-level actions for sensors going on or off, and actuators being turned on or off. There may also be higher level actions, such as a command to move an object from one location to another, a command to turn an entire subsystem on or off, or an event through which a subsystem indicates that an error has occurred.
- Synthesis-based engineering
-
A form of model-based engineering that uses supervisory controller synthesis (or simply supervisor synthesis) to automatically synthesize a correct-by-construction controller model.
- Supervisor
-
A maximally permissive controller model that may still allow multiple (safe) choices. Unlike a controller, it may for instance allow a choice between enabling multiple different actuators, or between enabling one actuator and disabling another one. When this distinction is not relevant, supervisor and controller are often used interchangeably.
- Supervisor synthesis
-
A correct-by-construction formal method that automatically synthesizes a supervisor. It involves the automatic generation, or synthesis, of a correct-by-construction controller model from a simple model of the to-be-controlled system and a model of the control requirements. This is also called controller synthesis or supervisory controller synthesis. Supervisor synthesis makes verification of the resulting supervisor model against the requirements from which it was synthesized superfluous. Validation of the resulting system being controlled by the controller (model) is still needed to ensure the specified requirements are indeed the desired requirements.
- Uncontrollable event
-
An event that operates autonomously, from the perspective of the controller. Such events are not controlled by the controller, which can thus not prevent them from occurring. For instance, events of a sensor could indicate that a button was pushed or released. And events of a movement limit sensor could indicate that a movement has reached the end position, or that the moving object is no longer at that position.
- Uncontrolled system / plant
-
The uncontrolled system is the system 'as is', without any control. It is also called a plant in control theory. For instance, at a low abstraction level, this could be the individual actuators and sensors of a system. At a higher abstraction level, it could be a collection of controllers for subsystems.