Module 4.1: User-specified requirements
A plant model contains all the system's behavior, including undesired behavior. In the previous module, we saw how certain undesired behavior, such as blocking behavior, is removed by synthesis. Besides such generally-applicable undesired behavior, systems typically also have system-specific undesired behavior. Often, two types of system-specific undesired behavior are recognized: unsafe behavior and unproductive behavior.
An example of unsafe behavior is when it is possible to open two opposite water lock gates simultaneously, causing a flood. Or, when two robots moving in the same space may collide, damaging them. And in a railway crossing system controlling a gate at a railway and a road intersection, it is unsafe if the gate is open, allowing road traffic to pass the intersection, if at the same time a train is at the intersection.
As an example of unproductive behavior, consider the following. In a factory, products first need to be processed, before they are checked to ensure that the processing was done correctly, and the products have the right quality. Robots take products from one place in the factory to another, taking them among others to the processing and checking stations. It is then unproductive if a robot takes an unprocessed product to the checking station, as it needs to first be processed before it is checked. Taking a product first to the checking station and then to the processing station, is not unsafe. However, it leads to unnecessary movements, prevents robots from performing productive movements, and overall makes the factory less efficient.
It is therefore important to define what the system is allowed to do or must never do, by defining requirements. Specifying requirements is an important part of synthesis-based engineering, as user-specified requirements, together with the plant model, form the input to the synthesis algorithm. It is important to specify requirements properly, as they directly affect the safety of the system. If you specify the wrong requirements, synthesis will still ensure that they are adhered to. However, you end up with a system that correctly satisfies the wrong requirements. Furthermore, mistakes in the form of design errors can be costly to correct later during the development process. But, specifying proper requirements is not so easy. It takes some practice.
Requirements can be specified in different ways, and later in this module you will learn about three of them: requirement automata, state requirement invariants, and state/event exclusion requirements invariants. Regardless of the form in which the requirements are specified, they all restrict the allowed behavior of the system. They either indicate what must never be allowed to happen, or they specify that only certain things are allowed to happen, meaning that all other things are disallowed. So, either restrictions are specified in a negative way, or in a positive way, but they are always restrictions nonetheless.
A trivial way to ensure that requirements are satisfied, is to not allow the system to perform any actions. For instance, if all safety requirements of a system are satisfied in the system's initial state, then a supervisor could restrict the behavior of the system to keep it forever in its initial state. For example, the gates of a water lock could be kept closed permanently. However, such severe restrictions would prevent the system from performing any useful behavior. Hence, synthesis still only restricts the behavior as much as is necessary to satisfy the requirements in every reachable state, prevent blocking situations, and prevent restricting uncontrollable events. Later in this module, we will adapt the synthesis algorithm for this.