Academic
Publications
On CSP Refinement Tests That Run Multiple Copies of a Process

On CSP Refinement Tests That Run Multiple Copies of a Process,10.1016/j.entcs.2009.08.011,Electronic Notes in Theoretical Computer Science,Gavin Lowe

On CSP Refinement Tests That Run Multiple Copies of a Process   (Citations: 2)
BibTex | RIS | RefWorks Download
In this paper we consider CSP stable failures refinement checks, where the right hand side of the refinement contains n copies of a process P. We show that such refinement checks capture precisely those predicates of the form 8f1,...,fn 2 failures(P) q R(f1,...,fn) for some n-ary relation R. The construction of the refinement test is, in general, infinitary; however, we show how, given R, one can often calculate a finite state refinement check.
Journal: Electronic Notes in Theoretical Computer Science - ENTCS , vol. 250, no. 1, pp. 153-170, 2009
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...Lowe [6] has shown that all binary failures properties can be expressed equivalently in the form of CSP renement tests; most of these tests are nite state, enabling them to be automatically tested by CSP’s renement checker FDR [4]...
    • ...Indeed, when RCFNDC and Non-Causation were rst proposed (in [7] and [10] respectively, before [6]), renement tests of this form were presented in order to facilitate the automatic verication of these properties...
    • ...The following is a slight adaptation of the Spec process derived in [6] for RCFNDC...

    Toby C. Murrayet al. On Refinement-Closed Security Properties and Nondeterministic Composit...

    • ...the identity expression as used in (2), or perhaps an expression that runs multiple copies of System in parallel as in [Low09])...
    • ...Similar arguments can be made to show that all of Lowe’s n-ary failures predicates [Low09], including allknownrefinement-closednoninterference[GM82]predicates(suchasLowe’sRCFNDC[Low07]andRoscoe’s Lazy Independence [Ros97, Sect...
    • ...12.4]), certain formulations of responsiveness [RSR04, Low09], determinism [Ros97, Laz99] and certain non-causation predicates [ML07], are also safety predicates...
    • ...In [Low09], Lowe considers the problem of how to express n-ary failures predicates as finitary refinement checks for FDR to carry out...
    • ...Lowe [Low09] focused on producing finitary refinement checks for n-ary failures properties, namely those for which the left- and right-hand sides are always finite state whenever the system being analysed is finite-state...
    • ...(Indeed, the refinement checkconstructedintheproofsofTheorems15and19arecertainlynotfinitary.)Thisisbecauseweareinterested inthelimitsofexpressiveness.AnobviousavenueforfutureworkwouldconsiderhowtoadaptLowe’sresultsand techniques from [Low09] to produce finitary refinement checks for safety predicates, and to characterise those safety predicates and liveness predicates that can, and cannot, be expressed in the form of finitary refinement ...

    Toby Murray. On the limits of refinement-testing for model-checking CSP

Sort by: