CIRCAL and the representation of communication, concurrency, and time

Reviewer: Martin Rem

CIRCAL is, like CCS [1], a calculus of communicating components. Different components can be assembled to form larger components. Communication is instantaneous and has no direction. CIRCAL distinguishes itself primarily from CCS in that it contains multipoint communication and, thus, multipoint synchronization. This introduces two kinds of concurrency: simultaneous events and unordered events. In CIRCAL these are different from each other: a component can be required to react differently to two stimuli if they occur simultaneously than if they occur one after the other. CIRCAL has four operators for the construction of components: guarding, deterministic choice, nondeterministic choice, and termination. A component constructed with the operator for deterministic choice can nevertheless be nondeterministic, since it may involve a choice between alternatives with equal guards. Components may be assembled into systems using an operator for concurrent composition. Internal communications in systems can be hidden by applying an abstraction operator. There is also a hiding operator, but that operator does not hide communications: it disallows them. The usefulness of this operator is not made clear. A number of simple examples of components and systems thereof are presented. The examples illustrate the calculus well. It is shown how CIRCAL can be used to demonstrate that systems meet their specifications. One expects, however, that the amount of formal manipulation required in such a demonstration will make more complicated examples rapidly undoable. Milne suggests resorting to mechanical verification—based on CIRCAL—for complex systems.