In [131] a proof outline logic is provided for concurrent programming with additional rules to perform real-time verification. The logic is defined using the maximal parallelism computational model.
Safety properties assert that something bad does not occur during a run of the system. For example, assume that we wish to prove that ¬Q never occurs during any run of the system. To prove this, the designer typically searches for an invariant I, that characterizes current and possibly past program states, and is not invalidated by system actions. If the invariant I holds in all initial states of the system, and I⇒Q is valid, then ¬Q never becomes true.
Timing properties can often be formulated as safety properties. For example, in a process control system the elapsed time between stimulus and response must be bounded by some time d. The ``bad thing'' (reaching time d before seeing the response) can be specified in terms of times at which various control points in the real-time program are reached.
A logic L to verify untimed safety properties can form the basis of a logic L' to verify timing properties. To do this, constructs must be added so that in L' the designer can specify in the predicates I and Q information about the times at which events of interest occur. It must also be possible to establish that the actions of the system do not invalidate the invariant I. This means that the rules of L have to be refined with information about execution times. In [131] such a proof outline logic (POL) is developed. Knowledge of the execution times of individual actions is needed to reason about timing properties.
POL is similar to the Hoare-style logic in [135], which augments each action with an assignment to a clock variable to keep track of elapsed time. In contrast, POL augments the assertion language with additional terms. This results in a more expressive language.
The assertional logic of Hooman in [51] (discussed above) deals with synchronous message passing and has no shared variables (which makes compositional reasoning easier). Only certain times can be recorded, e.g. times at which externally visible events (such as communication) can occur, and the times at which program execution starts and terminates. Information about control points cannot be specified because internal activities betray the internal structure of a component, which would destroy compositionality. Certain liveness proofs can also be made. In contrast, POL deals with shared variables, but then relaxes the compositionality requirement. Liveness proofs cannot be given. POL can also be used to represent synchronous communication. The two logics are therefore incomparable although both are assertional in style.
Another assertional logic which is being extended to deal with real-time is the temporal logic of actions discussed in [68]. A report on this work was not available at the time this survey article was written.