Extending hoare logic to real-time
- 1 November 1994
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in Formal Aspects of Computing
- Vol. 6 (Suppl 1) , 801-825
- https://doi.org/10.1007/bf01213604
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.Keywords
This publication has 16 references indexed in Scilit:
- Specification and Verification of an Atomic Broadcast ProtocolPublished by Springer Nature ,1995
- Compositional verification of a distributed real-time arbitration protocolReal-Time Systems, 1994
- A compositional approach to the design of hybrid systemsPublished by Springer Nature ,1993
- Hybrid systems in TLA+Published by Springer Nature ,1993
- Verification of real-time systems using PVSPublished by Springer Nature ,1993
- Putting time into proof outlinesPublished by Springer Nature ,1992
- An old-fashioned recipe for real timePublished by Springer Nature ,1992
- A calculus of durationsInformation Processing Letters, 1991
- On the Development of Reactive SystemsPublished by Springer Nature ,1985
- An axiomatic basis for computer programmingCommunications of the ACM, 1969