@techreport{fournet2004stuck-free,
author = {Fournet, Cédric and Hoare, Tony and Rajamani, Sriram and Rehof, Jakob},
title = {Stuck-Free Conformance Theory for CCS},
year = {2004},
month = {July},
abstract = {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.},
url = {http://approjects.co.za/?big=en-us/research/publication/stuck-free-conformance-theory-for-ccs/},
pages = {20},
edition = {Proceedings of the 16th International Conference on Computer Aided Verification (CAV'04)},
number = {MSR-TR-2004-69},
note = {Proceedings of the SIGCOMM 2005 Workshop on Delay Tolerant Networking},
}