Developing Proof Rules for Distributed Real-Time Systems
with PVS
Jozef Hooman
Appeared in: Proceedings Workshop on Tool Support for System
Development and Verification,
B. Buth, R. Berghammer, and J. Peleska (editors),
BISS Monographs, Volume 1,
Shaker Verlag, Aachen, pages 120-139, 1998.
ABSTRACT
In previous work, the verification
system
PVS
has been used to support an assertional method
for the specification and verification of distributed
real-time systems.
Essential part of the method is a compositional rule
for parallel composition.
In this paper we focus on the formalization of parallel
composition in PVS.
Two, equivalent, versions of the semantics of parallel
composition are formulated in the specification language
of PVS.
Based on this semantics,
several proof rules are shown to be sound, using the
interactive proof checker of PVS.
We indicate how the general framework can be
instantiated for a particular class of applications
by giving an axiomatization of asynchronous communication.
Postscript