Assumption-Commitment Support for CSP Model Checking

We present a simple formulation of Assumption-Commitment reasoning using CSP. In our formulation, an assumption-commitment style property of a process SYS takes the form COM SYS ASS, for some `assumption' and `commitment' processes ASS and COM . We state some proof rules that allow us to derive assumption-commitment style properties of a composite system from corresponding properties of its components, given appropriate side conditions. Most of the rules have a superficially appealing `homomorphic' quality, in the sense that the overall assumption and commitment processes are composed similarly to the overall system. We also present a `non-homomorphic' rule that corresponds quite well to proof rules of established assumption-commitment theory. The antecedants and side conditions are expressed as refinements that can be checked separately by the refinement-style model checker FDR. Examples are given to illustrate application of our theory.

• Type: Journal
• Year: 2008
• Where: JAR
• Authors: Nick Moffat, Michael Goldsmith
• Keywords: Assumption-commitment Style, Assumption-commitment Style Property, Form Com Sys, JAR 2008