Assumption-Commitment Support for CSP Model Checking

Abstract : 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 de document :
Communication dans un congrès
Stephan Merz and Tobias Nipkow. Automatic Verification of Critical Systems, Sep 2006, Nancy/France, pp.104-119, 2006, Automatic Verification of Critical Systems (AVoCS 2006)
Liste complète des métadonnées

Littérature citée [14 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00089499
Contributeur : Stephan Merz <>
Soumis le : vendredi 18 août 2006 - 20:00:33
Dernière modification le : mardi 19 décembre 2006 - 14:21:00
Document(s) archivé(s) le : mardi 18 septembre 2012 - 16:41:29

Identifiants

  • HAL Id : inria-00089499, version 1

Collections

Citation

Nick Moffat, Michael Goldsmith. Assumption-Commitment Support for CSP Model Checking. Stephan Merz and Tobias Nipkow. Automatic Verification of Critical Systems, Sep 2006, Nancy/France, pp.104-119, 2006, Automatic Verification of Critical Systems (AVoCS 2006). 〈inria-00089499〉

Partager

Métriques

Consultations de la notice

130

Téléchargements de fichiers

116