Skip to main content

TS

On the limits of refinement-testing for model-checking CSP

Authors

Toby Murray

NICTA

UNSW

University of Oxford

Abstract

Refinement-checking, as embodied in tools like FDR, PAT and ProB, is a popular approach for model-checking refinement-closed predicates of CSP processes. We consider the limits of this approach to model-checking these kinds of predicates.

By adopting Clarkson and Schneider's hyperproperties framework, we show that every refinement-closed denotational predicate of finitely-nondeterministic, divergence-free CSP processes can be written as the conjunction of a safety predicate and the refinement-closure of a liveness predicate. We prove that every safety predicate is refinement-closed and that the safety predicates correspond precisely to the CSP refinement checks in finite linear observations models whose left-hand sides (i.e. specification processes) are independent of the systems to which they are applied.

We then show that there exist important liveness predicates whose refinement-closures cannot be expressed as refinement checks in any finite linear observations model, divergence-strict model, or non-divergence-strict divergence-recording model, i.e. in any standard CSP model suitable for reasoning about the kinds of processes that FDR can handle, namely finitely-branching ones. These liveness predicates include liveness properties under intuitive fairness assumptions, branching-time liveness predicates and non-causation predicates for reasoning about authority. We conclude that alternative verification approaches, besides refinement-checking, currently under development for CSP should be further pursued.

BibTeX Entry

  @article{Murray_13,
    doi              = {10.1007/s00165-011-0183-6},
    journal          = {Formal Aspects of Computing},
    author           = {Murray, Toby},
    number           = {2},
    month            = feb,
    volume           = {25},
    year             = {2013},
    keywords         = {refinement-testing, expressiveness, csp, model-checking, hyperproperties.},
    title            = {On the Limits of Refinement-Testing for Model-Checking {CSP}},
    pages            = {219-256}
  }

Download

Served by Apache on Linux on seL4.