Responsiveness and stable revivals
Joy N. Reed, Andrew William Roscoe, Jane E. Sinclair · Formal Aspects of Computing · 2007
Abstract Individual components in an inter-operating system require assurance from other components both of appropriate functionality and of suitable responsiveness. 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. This work has led to the discovery of a new semantic model for CSP with respect to which such properties are fully abstract. We present the new stable revivals model and discuss implications for responsiveness checking.