On the design of reactive systems
BIT Numerical Mathematics, 28 (3):
581--604 (1988)DOI: 10.1007/BF01941136
Abstract
The notion of joint actions provides a framework in which the granularity of atomic actions can be refined in the design of concurrent systems. An example of a telephone exchange is elaborated to demonstrate the feasibility of this approach for reactive systems and to illustrate transformations that are justifiable in such a process. Particular problems arise when a refinement would allow new interleavings of semantically relevant events. The meaning of a reactive computation is specified in a way that makes this possible.