Extending hoare logic to real-time

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.