Isabelle/DC: Proof Assistant for Duration Calculus

Isabelle/DC is a proof assistant for the real-time logic Duration Calculus. Isabelle/DC is build upon the generic theorem prover Isabelle.

Duration Calculus was originally developed by Zhou, Hoare and Ravn [1]. DC is an interval logic where time is modelled by the real numbers and boolean functions of time are used to capture the state of real time systems. A concise reference to the foundation, development and properties of the logic is [2]. The development of Isabelle/DC is described in the PhD-thesis of Søren Heilmann [3].
 

News

Software for Isabelle/98

  • The software is available here (includes [3]).
  • Supporting software necessary to run Isabelle/DC is Isabelle98 and SVC, a decision procedure for real arithmetic.
    •

    Related links

    References

    1. Zhou Chaochen, C.A.R. Hoare, and Anders P. Ravn, A calculus of durations, Information Processing Letters, 40(5):269-276, 1992.
    2. Michael R. Hansen and Zhou Chaochen, Duration calculus, logical foundations, Formal Aspects of Computing, 9:283-303, 1997.
    3. Søren T. Heilmann, Proof Support for Duration Calculus, Department of Information Technology, Technical University of Denmark, PhD-thesis, January 1999.   Abstract , Postscript
    Søren Heilmann, e-mail:sth@sth.dk, last modified:2000-1-17