A calculus of durations. (English) Zbl 0743.68097

Zhou, Chaochen; Hoare, C. A. R.; Ravn, Anders P.

Inf. Process. Lett. 40, No. 5, 269-276 (1991).

Summary: The purpose of the calculus of durations is to reason about designs and requirements for time-critical systems, without explicit mention of absolute time. Its distinctive feature is reasoning about integrals of the duration of different states within any given interval. The first section introduces the running example, of leakage in a gas burner. The second section defines and axiomatizes the proposed calculus as an extension of interval temporal logic. The third section applies it to the problem described in the introduction. The fourth section briefly surveys alternative calculi.

MSC:

68Q60	Specification and verification (program logics, model checking, etc.)
68N99	Theory of software
03B45	Modal logic (including the logic of norms)

Keywords:

real-time systems; software engineering; specification languages; temporal logic

References:

[1]	Barringer, H.; Kuiper, R.; Pnueli, A., A really abstract concurrent model and its temporal logic, Proc. 13th ACM Symp. on the Principles of Programming Languages, 173-183 (1986)
[2]	Brien, S. M., A relational calculus of intervals, (M.Sc. Thesis (September 1990), PRG, Oxford University Computing Laboratory) · Zbl 0789.68091
[3]	Schneider, S., Correctness and communication of real-time systems, (Ph.D. Thesis 1989 (March 1990), Oxford University Computing Laboratory), Techn. Monograph PRG-84
[4]	Hale, R. W.S., Programming in temporal logic, (Ph.D. Thesis (October 1988), University of Cambridge)
[6]	Jahanian, F.; Mok, A. K.-L., Safety analysis of timing properties in real-time systems, IEEE Trans. Software Eng., 12, 9, 890-904 (1986)
[7]	He, Jifeng, Specification-oriented semantics for ProCos programming language \(PL^{time}\), ProCos Tech. Rept. PRG/OU HJF7, ESPRIT BRA 3104 (May 1991)
[8]	Koymans, R., Specifying real-time properties with metric temporal logic, J. Real-time Systems, 2 (1990)
[9]	Moszkowski, B., A temporal logic for multi-level reasoning about hardware, IEEE Comput., 18, 2, 10-19 (1985)
[10]	Pnueli, A.; Harel, E., Applications of temporal logic to the specification of real time systems, (Joseph, M., Lecture Notes in Computer Science. Lecture Notes in Computer Science, Proc. Symp. Formal Techn. in Real-Time and Fault-Tolerant Systems, 331 (1988), Springer: Springer Berlin), 84-98
[11]	Ravn, A. P.; Rischel, H., Requirements capture for embedded real-time systems, (Proc. of IMACS MCTS 91 Symp., Vol. 2 (1991), Villeneuve-d’Asq: Villeneuve-d’Asq France), 147-152
[12]	Reed, G. M.; Roscoe, A. W., Metric spaces as models for real-time concurrency, (Mathematical Foundations of Programming. Mathematical Foundations of Programming, Lecture Notes in Computer Science, 298 (1987), Springer: Springer Berlin), 331-343 · Zbl 0644.68040
[13]	Sørensen, E. V.; Ravn, A. P.; Rischel, H., Control program for a gas burner: Part 1: Informal requirements, ProCoS Case Study 1. ProCoS Case Study 1, Tech. Rept. ID/DTH EVS2, ESPRIT BRA 3104 (March 1990)
[14]	Sørensen, E. V., On the specification of dependability requirements involving time integration, ProCos Working Paper (October 1989)
[15]	Chaochen, Zhou; Hansen, M. R., A note on completeness of the Duration Calculus, ProCos Working Paper (February 1991)