Duration calculus, a logical approach to real-time systems

Abstract

The Duration Calculus (DC) represents a logical approach to formal design of real-time systems. DC is based on interval logic, and uses real numbers to model time, and Boolean-valued (i.e. 0,1-valued) functions over time to model states 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 fist 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. This paper will give a brief introduction to DC and also an overview of the research of DC.