Stuck-Free Conformance Theory for CCS
- Cédric Fournet ,
- Tony Hoare ,
- Sriram Rajamani ,
- Jakob Rehof
MSR-TR-2004-69 |
Proceedings of the SIGCOMM 2005 Workshop on Delay Tolerant Networking
We present a novel refinement relation (stuck-free conformance) for CCS processes, which satisfies the substitutability property: If an implementation I conforms to a specification S, then C[S] stuck-free implies C[I] stuck-free, on any selected names ~a and for all CCS contexts C. Stuck-freedom is related to the CSP notion of deadlock, but it is more discriminative by taking orphan messages in asynchronous systems into account. We prove that conformance is a precongruence, i.e., it is preserved by all CCS contexts, thereby supporting modular refinement. We distinguish conformance from the related preorders, stable failures refinement in CSP and refusal preorder in CCS. Finally, we consider a family of parameterized refinement relations that can be generated from the format of our definition of stuck-free conformance.