Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(1)
Right Hand Side
Related Publications
(1)
Authority Analysis for Least Privilege Environments
Subscribe
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
Edit
On CSP Refinement Tests That Run Multiple Copies of a Process
(
Citations: 2
)
BibTex

RIS

RefWorks
Download
Gavin Lowe
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 nary 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. 153170, 2009
DOI:
10.1016/j.entcs.2009.08.011
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.
(
www.sciencedirect.com
)
(
www.comlab.ox.ac.uk
)
(
web.comlab.ox.ac.uk
)
(
dx.doi.org
)
(
www.informatik.unitrier.de
)
(
linkinghub.elsevier.com
)
More »
Citation Context
(2)
...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 NonCausation 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. Murray
,
et al.
On RefinementClosed 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 nary failures predicates [
Low09
], including allknownrefinementclosednoninterference[GM82]predicates(suchasLowe’sRCFNDC[Low07]andRoscoe’s Lazy Independence [Ros97, Sect...
...12.4]), certain formulations of responsiveness [RSR04,
Low09
], determinism [Ros97, Laz99] and certain noncausation predicates [ML07], are also safety predicates...
...In [
Low09
], Lowe considers the problem of how to express nary failures predicates as finitary refinement checks for FDR to carry out...
...Lowe [
Low09
] focused on producing finitary refinement checks for nary failures properties, namely those for which the left and righthand sides are always finite state whenever the system being analysed is finitestate...
...(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 refinementtesting for modelchecking CSP
References
(9)
Comparing Two Information Flow Security Properties
(
Citations: 22
)
Riccardo Focardi
,
A. Zamboni
Conference:
Computer Security Foundations Workshop  CSFW
, pp. 116122, 1996
Communicating Sequential Processes
(
Citations: 6994
)
C. A. R. Hoare
Published in 1985.
On information o w and renemen tclosure
(
Citations: 5
)
Gavin Lowe
Conference:
Workshop on Issues in the Theory of Security  WITS
The Theory and Practice of Concurrency
(
Citations: 1023
)
A. W. Roscoe
Published in 1993.
On the expressive power of CSP refinement
(
Citations: 12
)
A. W. Roscoe
Journal:
Formal Aspects of Computing  FAC
, vol. 17, no. 2, pp. 93112, 2005
Sort by:
Citations
(2)
On RefinementClosed Security Properties and Nondeterministic Compositions
(
Citations: 2
)
Toby C. Murray
,
Gavin Lowe
Journal:
Electronic Notes in Theoretical Computer Science  ENTCS
, vol. 250, no. 2, pp. 4968, 2009
On the limits of refinementtesting for modelchecking CSP
Toby Murray
Journal:
Formal Aspects of Computing  FAC
, pp. 138