Programming Research Group Technical Monograph PRG-84

Steve Schneider

March 1990, 211 pages, ISBN 0-902928-63-5

This doctoral thesis builds upon the mathematical theory for real-time distributed computing developed by Reed and Roscoe. Time-critical process constructors for modelling time-outs, interrupts, and communication constructs, are defined in terms of the primitive operators of Timed Communicating Sequential Processes (TCSP). The work on communication involves the modelling of channels, inputs, outputs, chaining, and a characterisation and analysis of buffers. These tools are applied to the specification, construction, and verification of communication protocols. The methods are generalised to apply to networks.

Real-time systems are inherently complex, and this is reflected in the complexity of the verification process. This thesis presents three useful verification methods. The first is a complete compositional proof system for behavioural specifications on TCSP. The second involves the definition of generic specifications on processes, capturing those properties of component processes which combine readily when constructing large networks. Methods of constructing and identifying processes meeting such specifications are examined, and laws are formulated concerning their interaction.

The third approach exploits the mappings between different models within Reed's hierarchy. A notion of timewise refinement is presented which allows simple processes to be refined by the introduction of timing considerations. Properties which are preserved by timewise refinement are important, since there already exist well-established techniques for proving that such properties hold of processes in models lower in the hierachy.