Preface

Summary

REAL-TIME SYSTEMS

As computing devices become faster and more powerful, we find ourselves increasingly dependent upon systems which are difficult to understand and prone to failure. The failure of a commercial banking system or a company database may be expensive and inconvenient. The failure of an aircraft control system or a railway signalling network may result in injury or death. As the consequences of system failure become ever more severe, we must find ways to make these applications of computing technology safer and more reliable.

Over the past twenty-five years, mathematical techniques have been developed for the specification and implementation of computing systems. Formal methods have been used in the design and analysis of transformational systems—in which results are computed from a given set of inputs—and have been shown to reduce design costs and improve reliability. However, many of the systems in which safety is a primary concern are real-time systems, and cannot easily be viewed in a transformational setting.

Real-time systems maintain a continuous interaction with their environment and are often subject to complex timing constraints. They may also be required to perform several tasks concurrently. To reason about such systems we require a mathematical formalism that supports a treatment of timed concurrency. In this thesis we explore and extend one such formalism, the theory of Communicating Sequential Processes, first introduced by Hoare (1985).