Abstract
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 stuckfree, 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. © Springer-Verlag Berlin Heidelberg 2004.
Cite
CITATION STYLE
Fournet, C., Hoare, T., Rajamani, S. K., & Rehof, J. (2004). Stuck-free conformance. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3114, 242–254. https://doi.org/10.1007/978-3-540-27813-9_19
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
