A calculus of durations.

*(English)*Zbl 0743.68097Summary: 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

\textit{C. Zhou} et al., Inf. Process. Lett. 40, No. 5, 269--276 (1991; Zbl 0743.68097)

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.