Module 4.2: Requirement automata and invariants

As already mentioned in the previous sub-module, requirements can be specified in different ways. The two main forms are requirement automata and requirement invariants. And requirement invariants also come in two different forms: state requirement invariants and state/event exclusion requirements. These three forms of requirements all restrict the allowed behavior of the system, either by indicating what must never be allowed to happen, or by specifying that only certain things are allowed to happen, meaning that all other things are disallowed. Restrictions are thus specified in a positive or negative way, but they are always restrictions nonetheless.

Example

To explain the difference between the different forms of requirements, we will consider an example of bridge deck and traffic light, similar to the one from the first module. The bridge deck can be closed, partially open or fully open. The traffic light can be red or green. The plants of this system can be modeled as follows:

Together, these two components define the following state space for the uncontrolled system:

For safety reasons, we do not want the bridge deck to be partially or fully open while the light is green, as then cars could drive off the bridge into the water. This phrases the safety requirement negatively, by describing what is not allowed. This same requirement can also be phrased positively, in terms of what is allowed: the bridge deck may only be partially or fully open while the light is red. Alternatively, we could say that the bridge must be closed when the light is green.

Next, we will model this requirement in each of the three different forms.

Requirement automata

Requirements can be specified as requirement automata, similar to how plant automata can be specified. In fact, there is no difference in what can be modeled for plant and requirement automata, except that they are either indicated as being a plant or a requirement. Requirement automata thus have location and edges, and they can also have variables, guards, and updates. And it is possible to make requirement automaton definitions and instantiate them multiple times.

The purposes of plant and requirement automata are different. A plant automaton specifies what the system can do, while a requirement automaton specifies what it is allowed to do. As with all automata, they synchronize on shared events. This way, a requirement automaton may restrict the behavior of the system. That is, if a certain event in the alphabet of a requirement automaton is not possible in one of the locations of the requirement automaton, while it is allowed in the plant, then the requirement automaton imposes a restriction.

One way to make a requirement automaton is to take one or more plant automata, compute their state space, and remove some behavior from it. If we do that for the bridge deck and traffic light example above, we could make the following requirement automaton:

This is a copy of the combined state space of the bridge deck and traffic light plant components, with some behavior removed from it. The two states that are unsafe have been removed, as have all transitions to these states. What remains is the allowed behavior, described as a requirement automaton. Certain behavior is restricted. For instance, when the bridge deck is open and the traffic light is red, the traffic light is not allowed to be turned to green. Putting this requirement together with the plant, it restricts the behavior of the plant, ensuring that the controlled system can never get to the unsafe states.

State requirement invariants

Requirements can be also be specified by state requirement invariants, which are also called state invariant requirements or requirement state invariants. This form of requirements allows you to specify a condition, in the form of a predicate, that must hold in all states of the controlled system. Any state that does not adhere to this condition is deemed a bad state, and synthesis will ensure it can never be reached.

For instance, for the bridge deck and traffic light example, we could specify a state requirement invariants, with the following condition:

1. not ((BridgeDeck.PartiallyOpen or BridgeDeck.Open) and TrafficLight.Green)

This specifies that it must not be the case, that the bridge deck is partially open or fully open and at the same the traffic light is green. This is phrased negatively. We could also phrase it positively:

2. (BridgeDeck.Closed and TrafficLight.Green) or TrafficLight.Red

This specifies that it must always be the case that, either the bridge deck is closed and the traffic light is green, or the traffic light is red. It does not indicate what the bridge deck must be when the traffic light is red, and thus it may have any state that is possible in the plant. That is, if the traffic light is red, the bridge deck may be closed, partially open or fully open.

The two requirements have the same effect, but are phrased differently. In this case, the negative phrasing more directly indicates the bad states, while the positive phrasing prevents the use of the negation (not). The choice of how to write a requirement invariant depends on the modeler's preference. But, in general, you should opt for what is the most direct, simple and readable.

State/event exclusion requirement invariants

The third and final form of requirements is state/event exclusion requirement invariants, which are also called state/event exclusion invariant requirements or requirement state/event exclusion invariants. This form of requirements allow you to specify a condition, in the form of a predicate, that must hold for an event to be enabled or disabled in certain states. If the condition is for disabling an event, synthesis will ensure the event is disabled in all states where the predicate holds. If the condition is for enabling an event, synthesis will ensure the event is disabled in all states where the predicate doesn't hold, such that it is only enabled in states where the predicate holds.

For instance, for the bridge deck and traffic light example, we could specify the following state/event exclusion requirement invariants to disable certain events in certain states:

3. BridgeDeck.Closed and TrafficLight.Green disables partially_opened
4. BridgeDeck.PartiallyOpen or BridgeDeck.Open disables to_green

The first requirement disables the partially_opened event in the state where the bridge deck is closed and the traffic light is green. This prevents transitioning from the Closed/Green state to the PartiallyOpen/Green state. Similarly, the second requirement disables the to_green event in states where the bridge deck is partially open or fully open. It prevents transitioning from the PartiallyOpen/Red state to the PartiallyOpen/Green state, and from the Open/Red state to the Open/Green state.

The requirements above restrict only the direct transitions to bad states. Synthesis will prevent reaching those bad states, and thus any transitions from the bad states are also not possible. We may exploit this in phrasing requirements, which can help to make requirements simpler. For instance, the above two requirements could also be written as:

5. TrafficLight.Green disables partially_opened
6. BridgeDeck.PartiallyOpen or BridgeDeck.Open disables to_green

The first requirement is changed, by dropping the BridgeDeck.Closed part of the condition. It is fine to also disable the partially_opened event in the Open/Green state, as that is a bad state.

Besides that, predicates can often be written in different way by making use of the fact that only a limited number of locations are present in automata. The bridge deck being partially open or fully open is therefore the same as it not being closed. We may thus also write the above two requirements as:

7. not TrafficLight.Red disables partially_opened
8. not BridgeDeck.Closed disables to_green

Which of these forms is better, depends on the modeler's preference, and what is simpler and more readable.

Besides these different ways of writing the requirements in a negative form, indicating when the events are disabled, they can also be specified positively, indicating when the events are enabled/allowed:

9. partially_opened needs TrafficLight.Red
10. to_green needs BridgeDeck.Closed

This indicates that for the bridge deck to be partially opened, the traffic light needs to be red. If it is green, this event is thus not allowed. Similarly, for the traffic light to be turned to green, the bridge deck needs to be closed. If the bridge deck is partially or fully open, the light may thus not be turned to green.

As with state requirement invariants, which form to use, positive or negative, depends on preference and readability. A positively stated state/event exclusion requirement invariants e needs p (like 9 and 10 above) can always be phrased negatively as not p disables e (like 7 and 8 above), and vice versa.

Choosing the best requirement form

For the example above, the requirement automaton is arguably the least suited form. It requires modeling a full automaton, with four locations and even more edges. Also, it indicates what is allowed, which means you mentally have to check what is disabled, and thus what is expressed as a requirement.

The invariants are more succinct. The different forms of requirement invariants (1, 2, 3+4, 5+6, 7+8, or 9+10) have their pros and cons as well. Variants 9+10 are the shortest, but require a mental step to invert the conditions to see what is disabled. Variants 7+8 use double negations (not and disables) and are thus best avoided. Variants 5+6 directly indicate what is disabled, and are not much longer than 9+10, and are thus a good choice. Variants 3+4 are needlessly longer than 5+6 and are thus best avoid as well.

Variant 2 also requires mentally inverting the condition to see what states are being forbidden. Variant 1 is in that sense the better option, even though it uses a negation.

In the end, it is up to you to decide which form you think is the most intuitive. But, variant 1 and variants 5+6 could be seen as the best options for this particular example.

Requirement automata to specify order

In the previous example of a bridge deck and traffic light, the requirement automaton was not the best option. Let us now consider another example, of a railway crossing, where a requirement automaton could be a good option. A red light can be on, signaling that a train is coming, and is off otherwise. A barrier is closed if a train approaches, such that road traffic can't cross the tracks. Once the train has passed, the barrier opens again. The plant of this railway crossing can be modeled as follows:

The light is initially Off, but can be turned on. If it is On, it can be turned off again. And so on. The barrier is initially Open. It can be closed, opened, closed, opened, and so on.

Together, these two components have the following state space:

To prevents potential collisions of road traffic with trains, some of this behavior is to be prevented. That is, for safety reasons, we want the light to be turned on, before the barrier is opened. Then, only once the light is turned off again, should the barrier be opened again.

We could model this using the following requirement:

This is a simple requirement, that indicates the order in which the four controllable events are allowed to happen. State requirement invariants are not applicable here, as we do not wish to restrict the states of the plant, but only the transitions. State/event exclusion requirement invariants are an alternative, but it would require four of them, one per event. The requirement automaton could be seen as the best option here, as it most intuitively and directly specifies the allowed order of events.

Do note, that this particular example may be too restrictive in practice. It for instance does not allow turning off the light if it was turned on by mistake, at least not without first closing the barrier.

Quiz