Formal Software Specification Using RAISE	Course Descriptions	Design Calculi for Telecommunications	UNU-IIST Home
Duration Calculus: A Logical Approach to Real-Time Systems

II/2/1/2 Duration Calculus: A Logical Approach to Real-Time Systems

Duration Calculus: An Overview

The Duration Calculus (DC) is a formal system for the specification and design of real-time safety-critical systems. The DC was proposed by C. Zhou, C.A.R. Hoare and A.P. Ravn, and developed initially with several other colleagues in the ProCoS project (ESPRIT BRA 3104). Afterwards, it has been extended and further investigated by numerous researchers, and a number of them are staff and fellows of UNU/IIST where C. Zhou has led a research group working on DC for about four years.

The duration calculus is a modal logic for describing and reasoning about the real-time behaviour of dynamic systems, where states change over time and are represented by functions from time (reals) to the Boolean values (0 and 1).

It is an extension of Interval Temporal Logic (Moszkowski & Manna), but with continuous time, and uses integrated durations of states as interval temporal variables. Assuming finite variability of state functions, the axioms and rules of the DC constitute a complete logic (relative to Interval Temporal Logic).

The real-time requirements of some embedded systems (e.g. Gas Burner, Auto Pilot, Railway Crossing, Water Level Monitoring, etc.) have been specified and analysed using the DC. By considering equality and inequality relations to be states, the DC can accommodate differential equations in its logic, hence establishing an interface to control theory. The interface with program specifications is established by introducing the predicates of communication traces and ready sets as states. The duration calculus has also been used to define real-time semantics of communicating processes and to specify the mapping of processes to limited hardware resources (scheduling). By regarding the waveform propagated through a wire as a state, the DC can also be used to describe and reason about the real-time behaviours of circuits at the gate level, and give a mathematical definition of delay-insensitive circuits.

As shown above, the applications of the DC have been selected from some of the main areas of real-time systems design. In all the selected cases the calculus seems essential for capturing timing constraints at a comfortable level of abstraction and in a form which is readable as well as appropriate for reasoning about the constraints.

To cope with other aspects of real time systems, many variants of DC have been developed, such as The Mean Value Duration Calculus which captures instantaneous events, The Probabilistic Duration Calculus which is able to describe the dependability of the system, The Finite Divergence Model in the Duration Calculus to reason about systems which are not finitely variable, to name a few.

The decidability/undecidability issues for the DC have been examined. Model checking techniques based on linear programming are being developed. Mechanical provers for the DC based on the PVS theorem prover have also been developed.

Course Contents

1. Introduction

   • Motivation

   • Other Real-time Logics

2. Duration Calculus

   • Interval Temporal Logic

   • Syntax of DC

   • Semantics of DC

   • Inference Rules

3. Applications

   • Real-time Requirements Capture

   • Real-time Semantics

   • Verification of Scheduling Algorithms

   • Hybrid Systems

4. Variants of Duration Calculus

   • Extended Duration Calculus

   • Mean Value Calculus

5. Theoretical Aspects of DC

   • Consistency and Completeness

   • Decidability and Undecidability

6. Mechanical Support

Specific Information about the Course

Course Materials

A collection of papers on Duration Calculus is provided for each participant.

Course Length

The course lasts five days, with approximately six hours of lectures and examples sessions per day.

References

1. Zhou Chaochen, C.A.R. Hoare, A.P. Ravn: A Calculus of Durations, Information Processing Letter, 40, 5, pp. 269-276, 1991

2. A.P. Ravn, H. Rischel: Requirements Capture for Embedded Real-Time Systems, Proc. IMACS-MCTS'91 Symp. Modelling and Control of Technological Systems, Vol 2, pp. 147-152, Villeneuve d'Ascq, France, 1991

3. A.P. Ravn, H. Rischel, K.M. Hansen: Specifying and Verifying Requirements of Real-Time Systems, Proceedings of the ACM SIGSOFT'91 Conference on Software for Critical Systems, New Orleans, December 4-6, 1991, ACM Software Engineering Notes, Vol 15, No 5, pp 44-54, 1991 (accepted also for IEEE Trans. Software Eng., 1993)

4. J.U. Skakkebæk, A.P. Ravn, H. Rischel, Zhou Chaochen: Specification of Embedded Real-Time Systems, Proc. 4th Euromicro Workshop on Real-Time Systems, IEEE Press, pp 116-121, June 1992

5. D. Bjørner: Trustworthy Computing Systems, Proceedings of IEEE International Conference on SE, Melbourna, May, 1992

6. Zhou Chaochen, M.R. Hansen, A.P. Ravn, H. Rischel: Duration Specifications for Shared Processors, Proceedings of the Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, Nijmegen, January 1992, LNCS 571, pp 21-32, 1992

7. He Jifeng, J. Bowen: Time Interval Semantics and Implementation of a Real -Time Programming Language, Proceedings 4th Euromicro Workshop on Real-Time Systems, IEEE Press, June 1992

8. M.R. Hansen, Zhou Chaochen, J. Staunstrup: A Real-Time Duration Semantics for Circuits, Proceedings of the Workshop on Timing Issues in the Specification and Synthesis of Digital Systems, Princeton, March 1992

9. Zhou Chaochen, A.P. Ravn, M.R. Hansen: An Extended Duration Calculus for Hybrid Real-Time Systems, presented in the Workshop on Theory of Hybrid Systems, Lyngby, Denmark, 19-20 Oct. 1992

10. Zhou Chaochen, Li Xiaoshan: A Mean-Value Duration Calculus, UNU/IIST Report No. 5, Feb. 1993, to be submitted to the Hoare Festschrift

11. Liu Zhiming, A.P. Ravn, E.V. Sørensen, Zhou Chaochen: Towards a Calculus of Systems Dependability, presented in the Workshop o Theory of Hybrid Systems, Lyngby, Denmark, 19-20 Oct. 1992

12. M.R. Hansen, Zhou Chaochen: Semantics and Completeness of Duration Calculus, J.W. de Bakker, C. Huizing, W.-P. de Roever, G. Rozenberg, (Eds) Real-Time: Theory in Practice, REX Workshop, LNCS 600, pp 209-225, 1992

13. Zhou Chaochen, M.R. Hansen, P. Sestoft: Decidability and Undecidability Results for Duration Calculus, Proceedings of STACS '93. 10th Symposium on Theoretical Aspects of Computer Science, Würzburg, LNCS 665, Feb. 1993

14. J.U. Skakkebæk, P. Sestoft: Checking Validity of Duration Calculus Formulas, submitted to Conference on Computer-Aided Verification, Crete, June 1993

15. D.V. Hung and Z. Chaochen: Probabilistic Duration Calculus for Continuous Time, UNU/IIST Report No. 25, May. 1994

16. Zhou Chaochen, Dang Van Hung, Li Xiaoshan: A Duration calculus with Infinite Intervals, UNU/IIST Report No. 40, LNCS 965 pp 16-41, February 1995.

17. J.U. Skakkebæk, N. Shankar: Towards a Duration Calculus Proof Assistant in PVS. In Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 863, 1994.

18. M.R. Hansen, P.K. Pandya, and Zhou Chaochen. Finite divergence. Theoretical Computer Science, 138:113-139, 1995.

19. M.R. Hansen and Zhou Chaochen. Lecture Notes on the Logical Foundations of Duration Calculus. To appear in Formal Aspects of Computing, 1997.

20. Zheng Yuhua and Zhou Chaochen. A Formal Proof of the Deadline Driven Scheduler. In Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 863, 1994.

Duration Calculus: A Logical Approach to Real-Time Systems
Formal Software Specification Using RAISE	Course Descriptions	Design Calculi for Telecommunications	UNU-IIST Home