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

J.J.M. Hooman

doi:10.1109/EMWRT.1992.637476

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

J.J.M. Hooman

Algorithms

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

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.

Original language	English
Title of host publication	4th Euromicro Workshop on Real-Time Systems (ECRTS'92, Athens, Greece, June 3-5, 1992)
Publisher	IEEE Computer Society
Pages	86-91
ISBN (Print)	0-8186-2815-4
DOIs	https://doi.org/10.1109/EMWRT.1992.637476
Publication status	Published - 1992

Access to Document

10.1109/EMWRT.1992.637476

Cite this

@inproceedings{f3e768b6fcd84ba78417533668f2f13b,

title = "A compositional method for the top-down design of real-time systems",

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.",

author = "J.J.M. Hooman",

year = "1992",

doi = "10.1109/EMWRT.1992.637476",

language = "English",

isbn = "0-8186-2815-4",

pages = "86--91",

booktitle = "4th Euromicro Workshop on Real-Time Systems (ECRTS'92, Athens, Greece, June 3-5, 1992)",

publisher = "IEEE Computer Society",

address = "United States",

}

TY - GEN

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

AU - Hooman, J.J.M.

PY - 1992

Y1 - 1992

N2 - 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.

AB - 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.

U2 - 10.1109/EMWRT.1992.637476

DO - 10.1109/EMWRT.1992.637476

M3 - Conference contribution

SN - 0-8186-2815-4

SP - 86

EP - 91

BT - 4th Euromicro Workshop on Real-Time Systems (ECRTS'92, Athens, Greece, June 3-5, 1992)

PB - IEEE Computer Society

ER -

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

Abstract

Access to Document

Fingerprint

Cite this