Hostname: page-component-669899f699-tzmfd Total loading time: 0 Render date: 2025-04-30T01:24:22.751Z Has data issue: false hasContentIssue false

Models for CSP with availability information

Published online by Cambridge University Press: 21 November 2014

GAVIN LOWE*
Affiliation:
Department of Computer Science, University of Oxford, Wolfson Building, Parks Road, OX1 3QD, United Kingdom Email gavin.lowe@cs.ox.ac.uk.

Abstract

We consider models of CSP based on recordingavailability information, i.e. the models record what events could have been performed instead of those that were actually performed. We present many different varieties of such models. For each, we give a compositional semantics, congruent to the operational semantics, and prove full abstraction and no-junk results. We compare the expressiveness of the different models.

Type
Paper
Copyright
Copyright © Cambridge University Press 2014 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Article purchase

Temporarily unavailable

References

Andrews,G. R. (2000)Foundations of Multithreaded, Parallel, and Distributed Programming,Addison-Wesley.Google Scholar
Bolton,C. andLowe,G. (2004)A hierarchy of failures-based models.Electronic Notes in Theoretical Computer Science96129–152.CrossRefGoogle Scholar
de Nicola,R. andHennessy,M. C. B. (1984)Testing equivalences for processes.Theoretical Computer Science3483–133.Google Scholar
Formal Systems (Europe) Ltd. (2005)Failures Divergence Refinement – User Manual and Tutorial, Version 2.8.2.Google Scholar
Gibson-Robinson,T. (2010)Tyger: A Tool for Automatically Simulating CSP-Like Languages in CSP, Master's thesis, Oxford Universityhttp://www.cs.ox.ac.uk/files/4607/Thesis.pdf.Google Scholar
Hoare,C. A. R. (1985)Communicating Sequential Processes,Prentice Hall.Google Scholar
Lowe,G. (2009)Extending CSP with tests for availability. In:Proceedings of Concurrent Process Architectures,IOS Press325–348.Google Scholar
Milner,R. (1980)A Calculus of Communicating Systems. Springer Lecture Notes in Computer Science92.Google Scholar
Mukarram,A. (1993)A Refusal Testing Model for CSP, D. Phil thesis, Oxford.Google Scholar
Olderog,E. R. andHoare,C. A. R. (1983)Specification-oriented semantics for communicating processes. In:Diaz,J. (ed.) 10th ICALP.Lecture Notes in Computer Science154561–572.Google Scholar
Phillips,I. (1987) Refusal testing.Theoretical Computer Science.Google Scholar
Roscoe,A. W. (1994)Model-checking CSP. In:A Classical Mind, Essays in Honour of C. A. R. Hoare,Prentice-Hall353–378.Google Scholar
Roscoe,A. W. (1997)The Theory and Practice of Concurrency,Prentice Hall.Google Scholar
Roscoe,A. W. (2005)Seeing beyond divergence. In: Proceedings of ‘25 Years of CSP’.Lecture Notes in Computer Science352515–25.Google Scholar
Roscoe,A. W. (2009) On the expressiveness of CSP. Available viahttp://web.comlab.ox.ac.uk//files/1383/complete(3).pdf.Google Scholar
Roscoe,A. W. (2009)Revivals, stuckness and the hierarchy of CSP models.Journal of Logic and Algebraic Programming78(3)163–190.Google Scholar
Roscoe,A. W. (2010)Understanding Concurrent Systems,Springer.Google Scholar
van Glabbeek,R. J. (1993)The linear time–branching time spectrum II; the semantics of sequential systems with silent moves (extended abstract). In: Proceedings CONCUR'93, 4th International Conference on Concurrency Theory.Springer-Verlag Lecture Notes in Computer Science71566–81.Google Scholar
van Glabbeek,R. J. (2001)The linear time–branching time spectrum I; the semantics of concrete, sequential processes. In:Bergstra,J. A.,Ponse,A. andSmolka,S. A. (eds.)Handbook of Process Algebra,Elsevier chapter 1,3–99.CrossRefGoogle Scholar
Welch,P.,Brown,N.,Morres,J.,Chalmers,K. andSputh,B. (2007) Integrating and extending JCSP. In:Communicating Process Architectures 48–76.Google Scholar