The research described in this monograph concerns the formal specification and compositional verification of real-time systems. A real-time programming language is considered in which concurrent processes communicate by synchronous message passing along unidirectional channels. To specify functional and timing properties of programs, two formalisms are investigated: one using a real-time version of temporal logic, called Metric Temporal Logic, and another which is based on extended Hoare triples. Metric Temporal Logic provides a concise notation to express timing properties and to axiomatize...
The research described in this monograph concerns the formal specification and compositional verification of real-time systems. A real-time programmin...