[ Russian ] [ English ]

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.

Supported by Synthesis Group