Testing of safety properties

In our earlier work [JPVO95], a 5ESS developer had provided a summary of safety properties that this variation of the CGA software should satisfy. We consider some of the same safety properties here.

The actual timing constants have been omitted here due to proprietary considerations and have been denoted by symbols c_i. These are so-called ``soft'' real-time properties in the sense that the exact bounds c_i need not be satisfied; a reasonable approximation will do.

T0

A summary request must be completed in less than time c₁.

T1

If a queried processor does not reply within time c₂, the request should be aborted immediately and the next processor should be queried.

T2

If the HMI blocks on a message, the collection of new CGA data must suspend.

T3

If the HMI blocks on a message, the message should be resent with a period of time c₃, until the HMI unblocks. If time c₄elapses and the HMI has not yet unblocked, the summary request should be aborted.

T4

If HMI unblocks after CGA data collection has been suspended, CGA data collection must be reactivated immediately.

T5

No summary request should be honored when another summary request is currently running.

Using the specification-based testing facility of JavaTriveni, we have tested our JavaTriveni implementation of the CGA software against these properties. Since our JavaTriveni version used system timers to enforce timing constraints, our implementation can only be expected to satisfy the above properties under certain obvious assumptions about these system timers. In particular, we need to assume that when a timer is set with the value c_i, it either expires or is cleared within time c_i after it is set.