A compositional method for the top-down design of real-time systems

1 January 1992

conference paper
Published by Institute of Electrical and Electronics Engineers (IEEE)

p. 86-91
https://doi.org/10.1109/emwrt.1992.637476

Abstract

To specify and verify real-time systems, we consider a formalism based on Hoare triples (precondition, program, postcondition) which are extended with a third assertion, called commitment, to express the real-time communication interface of the program. In this paper we axiomatize concurrent programs that communicate by means of a common bus. To support top-down program Verification we formulate a compositional proof system for these extended Hoare triples. The method as illustrated by a distributed arbitration protocol.

Keywords

REAL TIME SYSTEMS
PROTOCOLS
MATHEMATICS
ELECTRONIC MAIL
TIMING
PARALLEL PROCESSING
PROCESSOR SCHEDULING
COMPUTER LANGUAGES
PETROLEUM

This publication has 1 reference indexed in Scilit:

An axiomatic basis for computer programming
Communications of the ACM, 1969