Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Stuck-Free Conformance Theory for CCS

Cedric Fournet, Tony Hoare, Sriram K. Rajamani, and Jakob Rehof

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.

Details

Publication typeTechReport
NumberMSR-TR-2004-69
Pages20
InstitutionMicrosoft Research
> Publications > Stuck-Free Conformance Theory for CCS