We present a novel refinement relation (stuck-free conformance) for CCS processes, which satisfies the substitutability property:
If I conforms to S, and P is any environment such that P | S is stuck-free, then P | I is stuck-free. 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 on CCS processes, thereby supporting modular
refinement. We distinguish conformance from the related preorders, stable failures refinement in CSP and refusal preorder
in CCS. We have implemented conformance checking in a new software model checker, zing, and we report on how we used it to find errors in distributed programs.