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

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › Academic › peer review

Samenvatting

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.

Originele taal-2	Engels
Titel	4th Euromicro Workshop on Real-Time Systems (ECRTS'92, Athens, Greece, June 3-5, 1992)
Uitgeverij	IEEE Computer Society
Pagina's	86-91
ISBN van geprinte versie	0-8186-2815-4
DOI's	https://doi.org/10.1109/EMWRT.1992.637476
Status	Gepubliceerd - 1992

Toegang tot document

10.1109/EMWRT.1992.637476

Citeer dit

@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

Samenvatting

Toegang tot document

Vingerafdruk

Citeer dit