Lecture Notes in Computer Science
1 primary work
Book 558
Specification and Compositional Verification of Real-Time Systems
by Jozef Hooman
Published 1 November 1991
The research described in this monograph concerns the formal
specification and compositional verification of real-time
systems. A real-time programminglanguage is considered in
which concurrent processes communicate by synchronous
message passing along unidirectional channels. To specifiy
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
basedon extended Hoare triples. Metric Temporal Logic
provides a concise notationto express timing properties and
to axiomatize the programming language, whereas Hoare-style
formulae are especially convenient for the verification of
sequential constructs. For both approaches a compositional
proof system has been formulated to verify that a program
satisfies a specification. To deduce timing properties of
programs, first maximal parallelism is assumed, modeling the
situation in which each process has itsown processor. Next,
this model is generalized to multiprogramming where several
processes may share a processor and scheduling is based on
priorities. The proof systems are shown to be sound and
relatively complete with respect to a denotational semantics
of the programming language. The theory is illustrated by an
example of a watchdog timer.
specification and compositional verification of real-time
systems. A real-time programminglanguage is considered in
which concurrent processes communicate by synchronous
message passing along unidirectional channels. To specifiy
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
basedon extended Hoare triples. Metric Temporal Logic
provides a concise notationto express timing properties and
to axiomatize the programming language, whereas Hoare-style
formulae are especially convenient for the verification of
sequential constructs. For both approaches a compositional
proof system has been formulated to verify that a program
satisfies a specification. To deduce timing properties of
programs, first maximal parallelism is assumed, modeling the
situation in which each process has itsown processor. Next,
this model is generalized to multiprogramming where several
processes may share a processor and scheduling is based on
priorities. The proof systems are shown to be sound and
relatively complete with respect to a denotational semantics
of the programming language. The theory is illustrated by an
example of a watchdog timer.