Machine-Verifiable Responsiveness

Individual components in an inter-operating system will require assurance both of appropriate functionality and of responsiveness from other components. We have developed properties which capture the notion of non-blocking responsive behaviour, together with machine-based checks implemented in the CSP model-checker, FDR. In this paper we illustrate the use of our responsiveness properties with a small example, and provide a detailed comparison to related work in CCS. To this end we develop a new model of CSP with respect to which such properties are fully abstract.