A compositional proof theory for real-time distributed message passing

J.J.M. Hooman

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

8 Citaten (Scopus)


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.
Originele taal-2Engels
TitelPARLE Parallel Architectures and Languages Europe
SubtitelVolume II: Parallel Languages Eindhoven, The Netherlands, June 15–19, 1987 Proceedings
RedacteurenJ.W. de Bakker, A.J. Nijman, P.C. Treleaven
Plaats van productieBerlin
Aantal pagina's18
ISBN van elektronische versie978-3-540-47181-3
ISBN van geprinte versie3-540-17945-3, 978-3-540-17945-0
StatusGepubliceerd - 1987

Publicatie series

NaamLecture Notes in Computer Science (LNCS)
ISSN van geprinte versie0302-9743

Vingerafdruk Duik in de onderzoeksthema's van 'A compositional proof theory for real-time distributed message passing'. Samen vormen ze een unieke vingerafdruk.

Citeer dit