An introduction to duration calculus
Zhou Chaochen,
United Nations University, Macao,
zcc@iist.unu.edu
The Duration Calculus (abbreviated DC) represents a logical approach
to formal design of real-time systems. DC is based on interval logic,
and uses the real numbers to model time, and Boolean-valued (i.e.
{0,1}-valued) functions over time to model states and events of
real-time systems. The duration of a state in a time interval is the
accumulated presence time of the state in the interval. DC extends
interval logic with a calculus to specify and reason about properties
of state durations.
The research of DC was introduced in the ProCoS project (ESPRIT BRA
3104 and 7071), when the project was investigating formal techniques
for designing safety critical real-time systems. In a project case
study of a gas burner system, it was realised that state duration had
not been well studied yet as an essential measurement of real-time
behaviour of computing systems. A research of a logic for state
durations was therefore initiated by the project in 1990.
The first paper of DC was published in 1991, and dozens of papers of
DC have been published since then, which cover developments of logical
calculi, their applications and mechanical support tools. The success
of DC also stimulates similar research in other formal approaches.
This introduction will emphasize mathematical models of real-time systems adopted by DC and their formalizations in interval logic.
|