Specification and Compositional Verification of Real-Time Systems

Appeared as volume 558 in the Lecture Notes in Computer Science series, Springer-Verlag, 1991.

ABSTRACT

Numerous formal methods have been devised to guarantee that a computer program performs the required task. These methods differ in many respects such as the class of programs to which the method does apply, the form of the correctness formulae used to specify and verify programs, and the class of properties that can be expressed. The aim of this work is to develop a formal framework for the specification and compositional verification of real-time embedded systems. Hence, in addition to the usual functional behaviour, also timing properties of programs are considered.