Trustworthy Systems

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,
    author           = {Murray, Toby},
    doi              = {10.1007/s00165-011-0183-6},
    journal          = {Formal Aspects of Computing},
    keywords         = {refinement-testing, expressiveness, csp, model-checking, hyperproperties.},
    month            = feb,
    number           = {2},
    pages            = {219--256},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/4907.pdf},
    title            = {On the Limits of Refinement-Testing for Model-Checking {CSP}},
    volume           = {25},
    year             = {2013}
  }

Download