×

zbMATH — the first resource for mathematics

A calculus of durations. (English) Zbl 0743.68097
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)
PDF BibTeX XML Cite
Full Text: DOI
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, () · Zbl 0789.68091
[3] Schneider, S., Correctness and communication of real-time systems, (), Techn. Monograph PRG-84
[4] Hale, R.W.S., Programming in temporal logic, ()
[5] J. Hooman and J. Widom, A temporal-logic based compositional proof system for real-time message passing, in: PARLE ’89, Lecture Notes in Computer Science \bf366 (Springer, Berlin).
[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, (), 84-98
[11] Ravn, A.P.; Rischel, H., Requirements capture for embedded real-time systems, (), 147-152
[12] Reed, G.M.; Roscoe, A.W., Metric spaces as models for real-time concurrency, (), 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, 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)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.