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 rul...
| Main Authors: | , |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
2008
|
| _version_ | 1797057795022913536 |
|---|---|
| author | Moffat, N Goldsmith, M |
| author_facet | Moffat, N Goldsmith, M |
| author_sort | Moffat, N |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-06T19:41:29Z |
| format | Journal article |
| id | oxford-uuid:20d28273-73c9-4f35-9408-12d6f46de1f1 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-06T19:41:29Z |
| publishDate | 2008 |
| record_format | dspace |
| spelling | oxford-uuid:20d28273-73c9-4f35-9408-12d6f46de1f12022-03-26T11:29:40ZAssumption-commitment support for CSP model checkingJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:20d28273-73c9-4f35-9408-12d6f46de1f1EnglishSymplectic Elements at Oxford2008Moffat, NGoldsmith, MWe 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. |
| spellingShingle | Moffat, N Goldsmith, M Assumption-commitment support for CSP model checking |
| title | Assumption-commitment support for CSP model checking |
| title_full | Assumption-commitment support for CSP model checking |
| title_fullStr | Assumption-commitment support for CSP model checking |
| title_full_unstemmed | Assumption-commitment support for CSP model checking |
| title_short | Assumption-commitment support for CSP model checking |
| title_sort | assumption commitment support for csp model checking |
| work_keys_str_mv | AT moffatn assumptioncommitmentsupportforcspmodelchecking AT goldsmithm assumptioncommitmentsupportforcspmodelchecking |