TY - JOUR
T1 - Unifying proof methodologies of duration calculus and timed linear temporal logic
AU - Liu, Zhiming
AU - Ravn, Anders P.
AU - Li, Xioshan
PY - 2004
Y1 - 2004
N2 - Linear Temporal Logic (LTL) has been widely used for specification and verification of reactive systems. Its standard model is sequences of states (or state transitions), and formulas describe sequencing of state transitions. When LTL is used to model real-time systems, a state is extended with a time stamp to record when a state transition takes place. Duration Calculus (DC), a dense time interval logic, is another well studied approach for real-time systems development. DC models behaviours of a system by functions from the domain of reals representing time to the system states, and properties are specified by formulas over time intervals. This paper extends this time domain to the Cartesian product of the real and the natural numbers in order to characterize both duration and transition properties of the computations of a system. With the extended time domain, a modest extension to the basic DC allows us to unify the methods from DC and LTL for formal real-time systems development: Requirements and high level design decisions are interval properties and are therefore specified and reasoned about in DC, while properties of an implementation, as well as the refinement relation between two implementations, are specified and verified compositionally and inductively in LTL. Implementation properties are related to requirement and design properties by rules for lifting LTL formulas to DC formulas. The method is illustrated by the Gas Burner case study.
AB - Linear Temporal Logic (LTL) has been widely used for specification and verification of reactive systems. Its standard model is sequences of states (or state transitions), and formulas describe sequencing of state transitions. When LTL is used to model real-time systems, a state is extended with a time stamp to record when a state transition takes place. Duration Calculus (DC), a dense time interval logic, is another well studied approach for real-time systems development. DC models behaviours of a system by functions from the domain of reals representing time to the system states, and properties are specified by formulas over time intervals. This paper extends this time domain to the Cartesian product of the real and the natural numbers in order to characterize both duration and transition properties of the computations of a system. With the extended time domain, a modest extension to the basic DC allows us to unify the methods from DC and LTL for formal real-time systems development: Requirements and high level design decisions are interval properties and are therefore specified and reasoned about in DC, while properties of an implementation, as well as the refinement relation between two implementations, are specified and verified compositionally and inductively in LTL. Implementation properties are related to requirement and design properties by rules for lifting LTL formulas to DC formulas. The method is illustrated by the Gas Burner case study.
M3 - Journal article
SN - 0934-5043
VL - 16
SP - 140
EP - 154
JO - Formal Aspects of Computing
JF - Formal Aspects of Computing
IS - 2
ER -