Responsiveness and stable revivals

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 modelchecker, 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 CSP with respect to which such properties are fully abstract. We present the new stable revivals model and discuss implications for responsiveness checking.

• Type: Journal
• Year: 2007
• Where: FAC
• Authors: Joy N. Reed, A. W. Roscoe, J. E. Sinclair
• Keywords: FAC 2007, Non-blocking Responsive Behaviour, Responsiveness, Suitable Responsiveness