Developing Proof Rules for Distributed Real-Time Systems
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.
In previous work, the verification
has been used to support an assertional method
for the specification and verification of distributed
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
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.