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
-
1999-5-23: This page constructed.
Software for Isabelle/98
Related links
-
PC/DC is another proof
assistant for Duration Calculus. It builds on PVS.
References
-
Zhou Chaochen, C.A.R. Hoare, and Anders P. Ravn, A calculus of durations,
Information Processing Letters, 40(5):269-276, 1992.
-
Michael R. Hansen and Zhou Chaochen, Duration calculus, logical foundations,
Formal
Aspects of Computing, 9:283-303, 1997.
-
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