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.


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.