Trustworthy Systems

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


Toby Murray



University of Oxford


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

    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         = {},
    title            = {On the Limits of Refinement-Testing for Model-Checking {CSP}},
    volume           = {25},
    year             = {2013}