Extending Hoare Logic to Real-Time
Jozef Hooman
Appeared in: Formal Aspects of Computing, Volume 6A, pages 801-825, 1994.
ABSTRACT
Classical Hoare triples are modified to specify and design
distributed real-time systems.
The assertion language is extended with primitives to express
the timing of observable actions.
Further the interpretation of triples is adapted such that both
terminating and nonterminating computations can be specified.
To verify that a concurrent program, with message passing along
asynchronous channels, satisfies a real-time specification,
we formulate a compositional proof system for our extended
Hoare logic.
The use of compositionality during top-down design
is illustrated by a process control example
of a chemical batch processing system.
Postscript