The Duration Calculus (DC) is an interval temporal logic for reasoning about real-time systems. We present a Gentzen-style sequent calculus for DC and a tool for constructing DC specifications and checking DC proofs. This tool is implemented by encoding the semantics of DC within a general-purpose specification and verification environment called PVS. In encoding DC, we have used PVS as a semantic logical framework, that is, we have employed the higher-order logic of PVS to define the semantics of DC and we have formally derived the DC inference rules using this semantic definition. The DC inference rules can then be used without any knowledge of the semantic encoding. The inference capabilities of PVS such as rewriting, decision procedures, and user defined proof strategies can be applied within DC proofs. The DC sequent calculus, the semantic encoding of DC in PVS, and the DC proof checking tool are illustrated using the example of a gas burner.

• csl-93-10.dvi
• csl-93-10.ps