Specification and Compositional Verification of Real-Time Systems

ISBN-13: 9783540549475 / Angielski / Miękka / 1991 / 242 str.

J. Hooman; Jozef Hooman

Opis

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 programming language, whereas Hoare-style formulae are especially convenient for the verification of sequential constructs.

Spis treści

Compositionality.- Compositionality and real-time.- Adding program variables.- Shared processors.- Concluding remarks.