Full abstraction of a denotational semantics for real-time concurrency
Cornelis Huizing, Rob Gerth, Willem Paul de Roever · TU/e Research Portal · 1986
We present a fully abstract semantics for real-time distributed computing of the Ada and OCCAM kind in a denotational style.This semantics tums tennination, communication along channels, and the time communication takes place, into observ-abIes.Yet it is the coarsest semantics to do so which is syntax-directed (this is known as full abstraction).It extends the linear history semantics for CSP of Francez, Lehman and Pnueli.Our execution model is based on maximizing concurrent activity as opposed to interleaving (in which only one action occurs at the time and arbitrary delays are incurred between actions).It is a variant of the maximal parallelism model of Salwicki and MUldner. 1 •.Introduction Although real-time embedded systems are surrounding us in a growing number of applications, little reflection has been given to the theoretical foundations of their design.Here, onl encounters problems of • language design: what are the right primitives for prescribing real-time computing; • semantics: what computational models underly real-time computing; • syntax-directed specification: how does one express the behaviour of real-time systems, so as to allow modular design; r This paper is based on C. Huizing's M.Sc.Thesis [HGR85].The authon arc working in and partially supported by Espri1 Project 937: Debugging and Specification« Real-Time ~beddcd Systems (DESCARTES).