PC/DC: The Proof Checker for Duration Calculus
PC/DC is the Proof Checker for Duration Calculus, a software tool used
to capture and verify properties of systems specified in the real time
logic Duration Calculus (DC). As a tool it builds heavily on the powerful
proof system PVS.
Duration Calculus was originally developed by Zhou, Hoare and Ravn .
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 .
PC/DC was originally developed by Jens Ulrik Skakkebæk for version
1 of PVS and described in his PhD-thesis . The advent of later versions
of PVS (PVS2a+, PVS2.1 and PVS2.2) has necessitated a port of the tool to this
new platform during which small improvements of the tool has been done
by Søren Heilmann.
2003-03-10: PC/DC for PVS 2.2 is now downloadable as a collection of smaller files, see the link below. Hopefully this will enable download from distant sites.
2003-03-02: PC/DC for PVS 2.2 is again available for downlaod. Use the links below.
2001-09-24: All links on this page to download PC/DC have gone stale. Mail me if you want a copy and I will try to dig it out from the archives.
1998-10-02: PC/DC release 981002 is now available for PVS 2.2. Get it below. The special DC parser is not longer a part of the tool. The PC/DC Users Guide describes the changes caused by this.
1998-09-25: It appears that PC/DC release 971012 does not work with the newly released PVS 2.2.
Software for PVS 2.2
Software for PVS 2.1
a program to check validity of discrete time Duration Calculus formulae.
It is developed by Paritosh K. Pandya, Tata Institute of Fundamental Research,
Methods page, maintained by Jonathan Bowen.
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.
JensUlrik Skakkebæk, A verification assistant for a real-time
logic, Technical Report 150, Dept. of Computer Science, Technical University
of Denmark, 1994,Ph.D. thesis.
Søren Heilmann, e-mail:firstname.lastname@example.org,