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

J.J.M. Hooman

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-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 languageEnglish
Title of host publication4th Euromicro Workshop on Real-Time Systems (ECRTS'92, Athens, Greece, June 3-5, 1992)
PublisherIEEE Computer Society
Pages86-91
ISBN (Print)0-8186-2815-4
DOIs
Publication statusPublished - 1992

Fingerprint

Real time systems
Network protocols
Communication

Cite this

Hooman, J. J. M. (1992). A compositional method for the top-down design of real-time systems. In 4th Euromicro Workshop on Real-Time Systems (ECRTS'92, Athens, Greece, June 3-5, 1992) (pp. 86-91). IEEE Computer Society. https://doi.org/10.1109/EMWRT.1992.637476
Hooman, J.J.M. / A compositional method for the top-down design of real-time systems. 4th Euromicro Workshop on Real-Time Systems (ECRTS'92, Athens, Greece, June 3-5, 1992). IEEE Computer Society, 1992. pp. 86-91
@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",

}

Hooman, JJM 1992, A compositional method for the top-down design of real-time systems. in 4th Euromicro Workshop on Real-Time Systems (ECRTS'92, Athens, Greece, June 3-5, 1992). IEEE Computer Society, pp. 86-91. https://doi.org/10.1109/EMWRT.1992.637476

A compositional method for the top-down design of real-time systems. / Hooman, J.J.M.

4th Euromicro Workshop on Real-Time Systems (ECRTS'92, Athens, Greece, June 3-5, 1992). IEEE Computer Society, 1992. p. 86-91.

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

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 -

Hooman JJM. A compositional method for the top-down design of real-time systems. In 4th Euromicro Workshop on Real-Time Systems (ECRTS'92, Athens, Greece, June 3-5, 1992). IEEE Computer Society. 1992. p. 86-91 https://doi.org/10.1109/EMWRT.1992.637476