Formal Specifications
Temporal logic is a prominent formal specification language for reactive systems. Linear time Temporal Logic (LTL) is the variant temporal logic most suitable for runtime monitoring. The syntax of LTL adds eight operators to the AND, OR, XOR, and NOT of propositional logic. Four of the operators deal with the future—Always in the Future, Sometime in the Future, Until, and Next Cycle. Four more address the past—Always in the Past, Sometime in the Past, Since, and Previous Cycle.
Metric Temporal Logic (MTL) enhances LTL's capability. With it, you can define upper and lower time constraints and time ranges for all LTL temporal operators. By imposing relative- and real-time constraints on LTL statements, MTL lets you use LTL to verify real-time systems.
An example showing a relative-time upper bound in MTL is: Always<10(readySignal Implies Next ackSignal), which says: Always, within the next 10 cycles, readySignal equals 1 implies that one cycle later ackSignal equals 1. readySignal and ackSignal are propositional logic expressions, and a cycle is an LTL time unit, which is a user-controlled quantity. For example, the infusion pump in Listing One was designed to operate and evaluate assertions at a rate of 1 Hz. The time constraint is relative in that it is counted in clock cycles.
Another example is Alwaystimer1[5,10](readySignal Implies Eventuallytimer2>= 20 ackSignal), which reads: Always, between 5 and 10 timer1 real-time units in the future, readySignal equals 1 implies that eventually, at least 20 timer2 real-time units further in the future, ackSignal equals 1. Here, two real-time constraints are specified by timer1 and timer2. A separate statement maps these timers to system calls, system clocks, or other counting devices.
Some code generators further extend LTL by adding counting operators (see "The Temporal Rover and the ATG Rover," by D. Drusinsky, Proceedings of the Spin2000 Workshop, Springer Verlag Lecture Notes in Computer Science). Another important extension is the support for asserting about time-series related properties, such as stability and monotonicity, as in an automotive cruise control system when required to sustain 98 percent speed stability while cruising.
—D.D.
