Extending Hoare logic to real-time

J.J.M. Hooman

Research output: Contribution to journalArticleAcademicpeer-review

31 Citations (Scopus)

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.
Original languageEnglish
Pages (from-to)801-825
JournalFormal Aspects of Computing
Volume6
Issue number6
DOIs
Publication statusPublished - 1994

Fingerprint

Dive into the research topics of 'Extending Hoare logic to real-time'. Together they form a unique fingerprint.

Cite this