Truth of Duration Calculus Formulae in Timed Frames

Article type: Research Article

Authors: Middelburg, Kees A.^;

Affiliations: Computing Science Department, Eindhoven University of Technology, Eindhoven, the Netherlands. keesm@win.tue.nl | Department of Philosophy, Utrecht University, Utrecht, the Netherlands. keesm@phil.uu.nl

Note: [] Address for correspondence: Computing Science Department, Eindhoven University of Technology, P.O. Box 513, 5600 MB Eindhoven, the Netherlands

Abstract: Duration calculus is a logical formalism designed for expressing and refining real-time requirements for systems. Timed frames are essentially transition systems meant for modeling the time-dependent behaviour of programs. We investigate the interpretation of duration calculus formulae in timed frames. We elaborate this topic from different angles and show that they agree with each other. The resulting interpretation is expected to make it generally easier to establish semantic links between duration calculus and formalisms aimed at programming. Such semantic links are prerequisites for a solid underpinning of approaches to system development that cover requirement capture through coding using both duration calculus and some formalism(s) aimed at programming.

Keywords: duration calculus, real-time requirements, timed frames, time-dependent behaviour, verification

DOI: 10.3233/FI-1998-36236

Journal: Fundamenta Informaticae, vol. 36, no. 2-3, pp. 235-263, 1998