A compositional proof theory for real-time distributed message passing

J.J.M. Hooman

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

8 Citations (Scopus)

Abstract

A compositional proof system is given for an OCCAM-like real-time programming language for distributed computing with communication via synchronous message passing. This proof system is based on specifications of processes which are independent of the program text of these processes. These specifications state (1) the assumptions of a process about the behaviour of its environment, and (2) the commitments of that process towards that environment provided these assumptions are met. The proof system is sound w.r.t a denotational semantics which incorporates assumptions regarding actions of the environment, thereby closely approximating the assumption/commitment style of reasoning on which the proof system is based. Concurrency is modelled as "maximal parallelism"; that is, if a process can proceed it will do so immediately. A process only waits when no local action is possible and no partner is available for communication. This maximality property is imposed on the domain of interpretation of assertions by postulating it as separate axiom. The timing behaviour of a system is expressed from the viewpoint of a global external observer, so there is a global notion of time. Time is not necessarily discrete.
Original languageEnglish
Title of host publicationPARLE Parallel Architectures and Languages Europe
Subtitle of host publicationVolume II: Parallel Languages Eindhoven, The Netherlands, June 15–19, 1987 Proceedings
EditorsJ.W. de Bakker, A.J. Nijman, P.C. Treleaven
Place of PublicationBerlin
PublisherSpringer
Chapter18
Pages315-332
Number of pages18
ISBN (Electronic)978-3-540-47181-3
ISBN (Print)3-540-17945-3, 978-3-540-17945-0
DOIs
Publication statusPublished - 1987

Publication series

NameLecture Notes in Computer Science (LNCS)
Volume259
ISSN (Print)0302-9743

Fingerprint

Message passing
Specifications
Communication
Distributed computer systems
Computer programming languages
Semantics
Acoustic waves

Cite this

Hooman, J. J. M. (1987). A compositional proof theory for real-time distributed message passing. In J. W. de Bakker, A. J. Nijman, & P. C. Treleaven (Eds.), PARLE Parallel Architectures and Languages Europe: Volume II: Parallel Languages Eindhoven, The Netherlands, June 15–19, 1987 Proceedings (pp. 315-332). (Lecture Notes in Computer Science (LNCS); Vol. 259). Berlin: Springer. https://doi.org/10.1007/3-540-17945-3_18
Hooman, J.J.M. / A compositional proof theory for real-time distributed message passing. PARLE Parallel Architectures and Languages Europe: Volume II: Parallel Languages Eindhoven, The Netherlands, June 15–19, 1987 Proceedings. editor / J.W. de Bakker ; A.J. Nijman ; P.C. Treleaven. Berlin : Springer, 1987. pp. 315-332 (Lecture Notes in Computer Science (LNCS)).
@inproceedings{1114de7a5ee049b0b17675f0bbc8a556,
title = "A compositional proof theory for real-time distributed message passing",
abstract = "A compositional proof system is given for an OCCAM-like real-time programming language for distributed computing with communication via synchronous message passing. This proof system is based on specifications of processes which are independent of the program text of these processes. These specifications state (1) the assumptions of a process about the behaviour of its environment, and (2) the commitments of that process towards that environment provided these assumptions are met. The proof system is sound w.r.t a denotational semantics which incorporates assumptions regarding actions of the environment, thereby closely approximating the assumption/commitment style of reasoning on which the proof system is based. Concurrency is modelled as {"}maximal parallelism{"}; that is, if a process can proceed it will do so immediately. A process only waits when no local action is possible and no partner is available for communication. This maximality property is imposed on the domain of interpretation of assertions by postulating it as separate axiom. The timing behaviour of a system is expressed from the viewpoint of a global external observer, so there is a global notion of time. Time is not necessarily discrete.",
author = "J.J.M. Hooman",
year = "1987",
doi = "10.1007/3-540-17945-3_18",
language = "English",
isbn = "3-540-17945-3",
series = "Lecture Notes in Computer Science (LNCS)",
publisher = "Springer",
pages = "315--332",
editor = "{de Bakker}, J.W. and A.J. Nijman and P.C. Treleaven",
booktitle = "PARLE Parallel Architectures and Languages Europe",
address = "Germany",

}

Hooman, JJM 1987, A compositional proof theory for real-time distributed message passing. in JW de Bakker, AJ Nijman & PC Treleaven (eds), PARLE Parallel Architectures and Languages Europe: Volume II: Parallel Languages Eindhoven, The Netherlands, June 15–19, 1987 Proceedings. Lecture Notes in Computer Science (LNCS), vol. 259, Springer, Berlin, pp. 315-332. https://doi.org/10.1007/3-540-17945-3_18

A compositional proof theory for real-time distributed message passing. / Hooman, J.J.M.

PARLE Parallel Architectures and Languages Europe: Volume II: Parallel Languages Eindhoven, The Netherlands, June 15–19, 1987 Proceedings. ed. / J.W. de Bakker; A.J. Nijman; P.C. Treleaven. Berlin : Springer, 1987. p. 315-332 (Lecture Notes in Computer Science (LNCS); Vol. 259).

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

TY - GEN

T1 - A compositional proof theory for real-time distributed message passing

AU - Hooman, J.J.M.

PY - 1987

Y1 - 1987

N2 - A compositional proof system is given for an OCCAM-like real-time programming language for distributed computing with communication via synchronous message passing. This proof system is based on specifications of processes which are independent of the program text of these processes. These specifications state (1) the assumptions of a process about the behaviour of its environment, and (2) the commitments of that process towards that environment provided these assumptions are met. The proof system is sound w.r.t a denotational semantics which incorporates assumptions regarding actions of the environment, thereby closely approximating the assumption/commitment style of reasoning on which the proof system is based. Concurrency is modelled as "maximal parallelism"; that is, if a process can proceed it will do so immediately. A process only waits when no local action is possible and no partner is available for communication. This maximality property is imposed on the domain of interpretation of assertions by postulating it as separate axiom. The timing behaviour of a system is expressed from the viewpoint of a global external observer, so there is a global notion of time. Time is not necessarily discrete.

AB - A compositional proof system is given for an OCCAM-like real-time programming language for distributed computing with communication via synchronous message passing. This proof system is based on specifications of processes which are independent of the program text of these processes. These specifications state (1) the assumptions of a process about the behaviour of its environment, and (2) the commitments of that process towards that environment provided these assumptions are met. The proof system is sound w.r.t a denotational semantics which incorporates assumptions regarding actions of the environment, thereby closely approximating the assumption/commitment style of reasoning on which the proof system is based. Concurrency is modelled as "maximal parallelism"; that is, if a process can proceed it will do so immediately. A process only waits when no local action is possible and no partner is available for communication. This maximality property is imposed on the domain of interpretation of assertions by postulating it as separate axiom. The timing behaviour of a system is expressed from the viewpoint of a global external observer, so there is a global notion of time. Time is not necessarily discrete.

U2 - 10.1007/3-540-17945-3_18

DO - 10.1007/3-540-17945-3_18

M3 - Conference contribution

SN - 3-540-17945-3

SN - 978-3-540-17945-0

T3 - Lecture Notes in Computer Science (LNCS)

SP - 315

EP - 332

BT - PARLE Parallel Architectures and Languages Europe

A2 - de Bakker, J.W.

A2 - Nijman, A.J.

A2 - Treleaven, P.C.

PB - Springer

CY - Berlin

ER -

Hooman JJM. A compositional proof theory for real-time distributed message passing. In de Bakker JW, Nijman AJ, Treleaven PC, editors, PARLE Parallel Architectures and Languages Europe: Volume II: Parallel Languages Eindhoven, The Netherlands, June 15–19, 1987 Proceedings. Berlin: Springer. 1987. p. 315-332. (Lecture Notes in Computer Science (LNCS)). https://doi.org/10.1007/3-540-17945-3_18