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
|