Reasoning About State Through Time

Working with before and after versions of state variables, unprimed and primed respectively (and remember they are separate variables in the model) can take some getting accustomed to, but it is a powerful technique for reasoning about use cases. It's basically the same technique physicists use when they talk about, say, the velocity of an object at time-zero with a variable like V⁰ versus the velocity at time-n with a variable like Vⁿ. Let's work through another example using this technique.

Use Case Overview

A manufacturing plant uses a storage tank to hold chemicals needed for its widget production; see Figure 5.7. The storage tank has a pipe through which the chemical flows to fill the tank and a pipe out of which the chemical flows to the machine that manufactures widgets. Rate of production by manufacturing determines the rate at which the chemical is needed and, hence, the rate of flow out of the tank. A new computer-based controller is being built to monitor levels in the tank, increasing or decreasing flow into the tank as needed. Sensors provide the controller with the current level in the tank, and the controller is programmed with a set target at which levels are ideally maintained in order to achieve a desired fluid pressure in the tank.

Figure 5.7. Chemical tank diagram showing flow in and flow out of the tank.

Figure 5.8 is the main scenario of the use case for maintaining the level of the chemical in the tank at the target level. The actor in this use case is the controller.

Figure 5.8. Main scenario, controller's use case for maintaining level of chemical in tank.

Use case description in hand, we are ready to think about how the controller might fail while executing this use case and identify preconditions that would guard against it.

Step 1. Find "Risky" Postconditions: Model as Equations

Clearly, controlling the rate of flow into the tank is the heart of this use case and a source of risk. Focusing on the control of this, we build a simple model of the postconditions of this facet of the use case (see Figure 5.9).

Figure 5.9. Model of main scenario for refilling chemical tank.

Step 2. Identify a Potential Failure: State an Invariant

There are two obvious failures this use case presents: failure to properly control the level resulting in the level dropping too low for manufacturing purposes or overfilling the tank resulting in a chemical spill.

From these potential failures, let's identify invariants, something that should always be true about the rates of flow into, and out of, the tank for this use case. In this use case, we have identified these state variables representing the rate of flow into and out of the tank at different points in time:

For this use case, the invariants of Figure 5.10 should always be true about these state variables; if postconditions of the use case violate them, the failures identified previously are possible outcomes.

Figure 5.10. Invariants that should always be true when refilling the tank.

We now have a model of the postconditions and invariants they should not violate (i.e., cause to fail). We are ready to calculate preconditions needed to guard the invariants.

Step 3. Calculate Preconditions

We now calculate the precondition for each of these invariants one at a time. Remember a precondition guards a specific invariant from one or more specific postconditions. They work as a unit. We start with InFlow' > OutFlow (see Figure 5.11).

Figure 5.11. Calculating the precondition to guard invariant InFlow' > OutFlow.

A precondition of Delta > 0 is intuitive and probably assumed. But, as noted previously, assumptions are often overlooked; from a testing perspective, one would want to ensure that the system checks for this case as ignoring it could eventually lead to depletion of chemicals in the tank.

Now we calculate the precondition for the next invariant, InFlow" < InFlow' (see Figure 5.12).

Figure 5.12. Calculate precondition to guard invariant InFlow'' < InFlow'.

What does OutFlow' < OutFlow + Delta as a precondition mean? This precondition has identified a potentially hazardous race condition in our use case. Because filling the tank takes time, the rate of flow out of the tank may change before the target level is reached. If, during the filling of the tank, OutFlow' increased to be equal to OutFlow + Delta, the level in the tank would stop rising, stabilize, and the use case would not terminate until the flow out changed again. If, during the filling of the tank, OutFlow' increased to be greater than OutFlow + Delta, the level in the tank would fall, potentially depleting chemicals in the tank. This precondition has identified that for the invariant to be met, OutFlow' can fluctuate up or down but only if it stays strictly less than OutFlow + Delta. Clearly such a race condition cannot be allowed and something will need to be done to prevent this (e.g., some semaphore or constraint mechanism to prevent variance in the flow out of the tank caused by manufacturing while the use case is in progress).

In short, this precondition has found the holy grail of test cases: a defect found before it reaches code!