Specification and Proof in Real−Time Systems

Abstract

This thesis shows how the mathematical theory of Timed Communicating Sequential Processes (Timed CSP) developed by Reed and Roscoe may be applied to the specification and proof of complex real-time systems. A number of substantial additions are made to the theory, producing a powerful tool for the analysis and implementation of timing requirements and concurrency. The syntax and semantics of Timed CSP are extended to include new primitive operators for timing and recursion. A language of behavioural specifications is formulated, together with a complete, compositional proof system. A significant case study is used to illustrate these developments. The language is then extended to include an element of broadcast concurrency.