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 [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].

PC/DC was originally developed by Jens Ulrik Skakkebæk for version 1 of PVS and described in his PhD-thesis [3]. 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.

News

• 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

Related links

• DCVALID is a program to check validity of discrete time Duration Calculus formulae. It is developed by Paritosh K. Pandya, Tata Institute of Fundamental Research, India.
• Formal Methods page, maintained by Jonathan Bowen.

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. 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.