Temporal Logic

Time is one of the critical issues in distributed systems, but it is not handled well with most specification techniques. We have found that interval temporal logic is useful in expressing temporal relationships. The operators of temporal logic allow concepts of time ordering to be expressed and reasoned about. Interval temporal logic allows concepts about time periods, as opposed to specific points in time, to be expressed. For example, the before(a,b) states that in the time period before event b happened, condition a was true.

The time periods about which we are reasoning must be appropriate to the problem at hand. Two distinctly different time periods are used in computer-based systems. One is real calendar time that is represented in domain objects. This is usually in the form of dates. The second type of time period is execution time. In object-oriented systems, this is often related to the lifetime of an object. This will be where we focus most of our discussion.

Temporal logic operators have been used implicitly for a long time. The always operator is an implicit part of every class invariant. Remember that the class invariant is a statement of those properties that are always true. The pre-condition is implicitly a before condition.

A few of the temporal operators that we have found useful include the following:

• before(a, b) a is true before event b occurs

• until(a, b) a is true until event b occurs

• after(a, b) a is true after event b occurs

An interval temporal operator applies for some period of time. Therefore, a test that seeks to verify that the implementation satisfies such a requirement must cover this interval. So how do you test something like the invariant

always(x >=0)

We handle this by repeatedly testing the validity of the invariant statement during all of our class tests. Always is interpreted as anytime that there is an instance object alive. Part of the behavioral specification for Timer objects might state the following:

After it is started, the Timer instance sends tick() messages to every registered listener until it is stopped.

It is fairly easy to test this at the class level, but it does require special handling. In the case of Timer, the test harness should inherit from TimeObservable so that it can be registered with the Timer instance. The test harness would do the following:

• Register itself with the Timer instance.

• Check that no tick() messages are being received.

• Send the start() message to the Timer instance.

• Check that tick() messages are being received.

• Send the stop() message to the Timer instance.

• Verify that no tick() messages are being received.

This basic test case should be repeated for a variety of time intervals between the various messages. A StopWatchTimer would be used to tell the test harness when to move to the next step.

To test that a temporal constraint is not violated, you can use two approaches. The first is to encapsulate the object on which the constraint is written. Then any access to the state about which the constraint applies can be monitored. After the access, the validity of the constraint is checked. The disadvantage of this is the possibility of altering the operation of the object by the instrumentation. We will consider this in the next section.

The second approach, as previously illustrated with Timer objects, is to sample over the interval about which the constraint is written. The intervals over which we normally sample would be the following:

• an interval in which a beginning time and an ending time are specified

• from instance creation until a specified time

• from a specified time until object destruction

Note that when we say a "specified time," it is usually specified as the occurrence of a specific event. The specified time is just whenever that event occurs.

Class and Object Invariants

We would like to make a distinction here between the class and object invariants that parallels our earlier distinction between class objects and instance objects. There can be a "class invariant" that corresponds to the class object and an "instance invariant" that corresponds to the instance objects. Basically, an invariant is any statement that should always be true when the subject of the invariant is in a steady state. We can also have system invariants. For example, the Singleton design pattern requires that there should only ever be at most one instance of the class. The class invariant would be

 number of instances < = 1 

The instance invariant would be related to the semantics of the domain. The instance object has no idea about the number of instances that can be created and its invariant shouldn't address that issue.

Please note that this is not accepted terminology in the industry, but hopefully it will make you think about the precise expression of invariants.

Temporal Test Patterns

In this section we will present three test patterns written in an informal style for the sake of space.

When a postcondition or a semantic description includes constraints written using temporal logic, new test conditions must be satisfied. In general, temporal constraints impose time requirements on the testing process. As a result, the parallel architecture for component testing (PACT) objects that exercise these tests will need to maintain their own threads of control so that they can independently act over an interval of time. In most cases those intervals are not based on clock time (although in a real-time system they might be), but rather the interval is from some event such as a method that has been completing until some event occurs. The PACT object will have to spawn observer objects to monitor the OUT.

The following are three of the operators that were previously defined and descriptions of how we have been successful in testing them.

Eventually(p)

Eventually, the postcondition of b.x(), p, will be true, but the temporal constraint is part of the postcondition of a.y(). It states a condition that will become true sometime in the future. The "future" is relative to the lifetime of a.y(). Anything that happens after a.y() terminates is in a's future.

Testing this condition obviously requires delaying the decision as to whether p is satisfied. The test must be conducted in the future of a.y(). In this situation, the PACT object for a is placed in a context that will last as long as the context for b. The PACT object has a separate thread. Periodically the a PACT object wakes up and sends messages to b to determine whether b.x() has completed execution. When it is determined that b.x() has occurred, the PACT object logs the fact and uses the results from the other portions of the postcondition of a.y() to determine whether the entire postcondition is satisfied. It then logs that result as well.

Figure 8.4. Eventually(b.x())

The PACT object continues to interrogate the b object until either b.x() occurs and p can be evaluated or b is deleted. If it is still checking when b is deleted, the PACT object logs a failure.

Until(p,q)

Until b.x(), b is in a state s₁. This is stated as until(s1, b.x()). To validate that this constraint holds, we need to test from the point that this assertion remains active until the b.x() event occurs. The PACT object is "fired off" at the moment the constraint becomes effective. It then periodically wakes up and checks the condition.

In the case of until, we need to determine that the condition "b is in s₁" is true every instant in time "until" the occurrence of the specified event. With eventually, we only evaluate the truth value of the condition once, after the event occurs, but with until we must continuously evaluate the condition "until" the specified event. If it evaluates to true every time until the terminal event, then the constraint is satisfied.

We obviously can't check the truth value continuously or no other work would get done in the system! If we check only at the time that the event occurs, we can't be certain what value the constraint had previous to that time, and the constraint doesn't say what should happen after the event has happened. The PACT object tester has to check previous to the event occurring. Checking once is hardly sufficient. Basically, we set the interval when the PACT object is created. The shorter the interval, the more certain the evaluation.

Figure 8.5. Until(b.x(),s1)

Always (p)

The always temporal operator is the most heavily used of the operators because every class invariant is essentially an always constraint. The always constraint says that at any point in the b swimlane, the logical constraint statement p is true.

Always as a class invariant refers to a time interval that corresponds to the lifetime of each instance of the class. As we stated about until, we cannot test continuously. We compromise by sampling periodically and evaluating the truth value at each time. In Chapter 5, we talked about testing for the class invariant at the end of each test case. This is the sampling technique we use as a default: test with each test method invocation. The potential problem is that a test case may cause several methods to be invoked. This is why we even call the invariant evaluation method multiple times in a test case method if the test case directly invokes multiple methods on the OUT.

Each temporal operator imposes different testing conditions, but each time the operator is used it follows the same basic pattern. The basic principles we have presented here should provide a basis for you to create your own test patterns.