7.1 Safety

7.1 Safety

In the previous chapter, we saw that the LTSA analysis tool performs deadlock analysis using a breadth-first search on the labeled transition system corresponding to an FSP model. The “bad” states that are the objective of this search are those states with no outgoing transitions, i.e. deadlock states. In addition to deadlock states, the search is looking for ERROR states. These are distinguished in the LTS by having a unique identity (–1). So far in the book, we have used the ERROR state explicitly denoted by the local process ERROR. In Chapter 4, we specified a test process that explicitly caused a transition to ERROR when it detected erroneous behavior. In Chapter 5, the ERROR state was used to detect when a finite range was exceeded. The example given in Figure 7.1 is an actuator that must not receive a second command before it has responded to the first.

Figure 7.1: ACTUATOR LTS.

With no control system to ensure that the actuator does not receive multiple unacknowledged commands, safety analysis performed by LTSA produces the following trace:

 Trace to property violation in ACTUATOR:      command      command

In the test process of Chapter 4, the range excess of Chapter 5 and the actuator example of Figure 7.1, we have specified the situations regarded as errors rather than directly expressing the required safety property that we wish to preserve. In the actuator example, the safety property is that a command action must always be followed by a respond action without an intervening command. In complex systems it is usually better to specify safety properties by stating directly what is required rather than stating what is not required. In this way, we can concentrate on the desired behavior of a system rather than trying to enumerate all the possible undesirable behaviors.

7.1.1 Safety Properties

Safety properties are specified in FSP by property processes. Syntactically, these are simply FSP processes prefixed by the keyword property. They are composed with a target system to ensure that the specified property holds for that system. The example of Figure 7.2 specifies the property that it is polite to knock before entering a room.

Figure 7.2: property POLITE.

The LTS diagram of Figure 7.2 reveals that in translating a property process, the compiler automatically generates the transitions to the ERROR state. It is easily seen that an enter action before a knock action causes a transition to the ERROR state. In addition, knocking twice is a violation of the POLITE property. It should be noted that in every state of the property process of Figure 7.2, all the actions in its alphabet (enter,knock) are eligible choices. Those that are not part of the behavior allowed by the safety property are transitions to the ERROR state. This is true of all property processes.

The property to check the correct operation of the ACTUATOR of Figure 7.1 is simply:

 property SAFE_ACTUATOR      =(command->respond->SAFE_ACTUATOR).

Property processes may be composed with a system without affecting the correct behavior of that system. In other words, composing a property process with a set of processes does not affect their normal operation. However, if behavior can occur which violates the safety property, then a transition to the ERROR state results. To preserve this transparency of safety properties, property processes must be deterministic. That is they must not contain non-deterministic choices. Experience has shown that this is rarely a restriction in practice.

A safety property P defines a deterministic process that asserts that any trace including actions in the alphabet of P, is accepted by P.

Thus, if P is composed with S, then traces of actions that are in the alphabet of S and the alphabet of P, must also be valid traces of P, otherwise ERROR is reachable. We can specify that an action or a set of actions should never happen by using alphabet extension. The example of Figure 7.3 asserts that disaster should never happen.

Figure 7.3: property CALM.

7.1.2 Safety Property for Mutual Exclusion

Listed below is a slightly modified version of the SEMADEMO model used in section 5.2.1 to show how semaphores are used to ensure mutual exclusion. The modification is to replace the single action critical with the actions enter and exit which model the entry and exit to the critical section in which mutually exclusive access to a shared resource is required.

 LOOP =     (mutex.down->enter->exit->mutex.up->LOOP). ||SEMADEMO = (p[1..3]:LOOP               ||{p[1..3]}::mutex:SEMAPHORE(1)).

To verify that this system does in fact ensure mutual exclusion, we can specify a mutual exclusion property and compose it with the system as follows:

 property MUTEX =       (p[i:1..3].enter->p[i].exit->MUTEX). ||CHECK = (SEMADEMO || MUTEX).

The safety property MUTEX specifies that when a process enters the critical section (p[i].enter), the same process must exit the critical section (p[i].exit) before another process can enter. The property is not violated in the system as it stands; however, if we change the value with which the semaphore is initialized from one to two (i.e. SEMAPHORE(2)) then safety analysis using LTSA produces the following trace:

 Trace to property violation in MUTEX:      p.1.mutex.down      p.1.enter      p.2.mutex.down      p.2.enter

The trace is clearly a violation of mutual exclusion since two processes have entered the critical section.