Assumption-commitment support for CSP model checking

We present a simple formulation of Assumption-Commitment reasoning using CSP (Communicating Sequential Processes). An assumption-commitment style property of a process SYS takes the form COM SYS ∥ ASS, for 'assumption' and 'commitment' processes ASS and COM. We describe proof rules that allow derivation of assumption-commitment style properties of a composite system from such properties of its components, given appropriate side conditions. Most of the rules have a superficially appealing 'homomorphic' quality: the overall assumption and commitment processes are composed similarly to the overall system. We also give a 'non-homomorphic' rule that corresponds quite well to classical assumption-commitment rules. Antecedants and side conditions can be expressed as refinements and checked separately by the refinement-style model checker FDR. Examples illustrate application of our theory. © 2008 Springer Science+Business Media B.V