Modelling coordinated atomic actions in timed CSP

Abstract

This paper proposes a formal framework for modelling the interaction of concurrent items of equipment in real-time safety-critical systems and reasoning about their behaviour abstractly. The framework is based on the concept of Coordinated Atomic (CA) actions, an approach widely used for structuring complex activities in fault-tolerant computer systems. It advocates a hierarchical approach and begins with the construction of a mathematical model of the behaviour of an individual item of equipment. Later on, the model is extended to incorporate the concept of a CA action. In the final stage, a formal representation of the ideal behaviour of an abstract CA action is provided. The framework uses Timed CSP - a well-established formalism used for representation and reasoning in real-time systems.