Compositional Verification of Real-Time Applications

Jozef Hooman

Appeared in: Proceedings Compositionality - The Significant Difference (COMPOS '97), LNCS 1536, Springer-Verlag, pp. 276-300, 1998.

ABSTRACT

To support top-down design of distributed real-time systems, a framework of mixed terms has been incorporated in the verification system PVS. Programs and assertional specifications are treated in a uniform way. We focus on the timed behaviour of parallel composition and hiding, presenting several alternatives for the definition of a denotational semantics. This forms the basis of compositional proof rules for parallel composition and hiding. The formalism is applied to an example of a hybrid system, which also serves to illustrate our ideas on platform-independent programming.