Assumption-Commitment Support for CSP Model Checking - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2006

Assumption-Commitment Support for CSP Model Checking

Nick Moffat
  • Fonction : Auteur
  • PersonId : 834685

Résumé

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.
Fichier principal
Vignette du fichier
MoffatG_AC_AVoCS_2006.pdf (224.54 Ko) Télécharger le fichier
Loading...

Dates et versions

inria-00089499 , version 1 (18-08-2006)

Identifiants

  • HAL Id : inria-00089499 , version 1

Citer

Nick Moffat, Michael Goldsmith. Assumption-Commitment Support for CSP Model Checking. Automatic Verification of Critical Systems, Sep 2006, Nancy/France, pp.104-119. ⟨inria-00089499⟩

Collections

AVOCS06
84 Consultations
188 Téléchargements

Partager

Gmail Facebook X LinkedIn More