CORRECTNESS AND COMMUNICATION IN REAL−TIME SYSTEMS

Abstract

This thesis builds upon the mathematical theory for real-time distributed computing developed by Reed and Roscoe. Time-critical process constructors for modelling timeouts, 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.