Specification and Compositional Verification of Real-Time Systems
Appeared as volume 558 in the Lecture Notes in Computer Science series, Springer-Verlag, 1991.
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