A Theory of Communicating Sequential Processes

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A Theory of Communicating Sequential Processes

Full text

Pdf (1.84 MB)

Source

Journal of the ACM (JACM) archive
Volume 31 , Issue 3 (July 1984) table of contents

Pages: 560 - 599

Year of Publication: 1984

ISSN:0004-5411

Authors

S. D. Brookes	Carnegie-Mellon Umversity, Pittsburgh, Pennsylvania
C. A. R. Hoare	Oxford Umversity Programmmg Research Group, Oxford, England
A. W. Roscoe	Oxford Umversity Programmmg Research Group, Oxford, England

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 29, Downloads (12 Months): 239, Citation Count: 85

Additional Information:

abstract references cited by index terms review collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/828.833 What is a DOI?

ABSTRACT

A mathematical model for communicating sequential processes is given, and a number of its interesting and useful properties are stated and proved. The possibilities of nondetermimsm are fully taken into account.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Krzysztof R. Apt , Nissim Francez , Willem P. de Roever, A Proof System for Communicating Sequential Processes, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.3, p.359-385, July 1980 [doi>10.1145/357103.357110]
	2	BROOKES, S.D.Amodel for eommumcating sequential processes. D.Phil. d~ssertation, Oxford Univ., Oxford, England, 1983.
	3	Stephen D. Brookes, On the Relationship of CCS and CSP, Proceedings of the 10th Colloquium on Automata, Languages and Programming, p.83-96, July 18-22, 1983
	4	Stephen D. Brookes, A Semantics and Proof System for Communicating Processes, Proceedings of the Carnegie Mellon Workshop on Logic of Programs, p.68-85, June 06-08, 1983
	5	BROOKES, S.D., AND ROSC'OE, A.W. An improved failures model for communieattng processes, to be published as CMU Teeh. Rep., 1984.
	6	K. M Chandy , Jayadev Misra, An Axiomatic Proof Technique for Networks of Communicating Processes, University of Texas at Austin, Austin, TX, 1979
	7	DI/KSTRA, E.W.Cooperating sequential processes. In Programmmg Languages, F. Genuys, Ed. Academic Press, New York, 1968.
	8	FRANCEZ, N., LEHMANN, D., AND PNEULI, A. A linear history semantics of languages for dJstnbuted programming. In Proceedings of the 21st IEEE Foundations of Computer Science Symposium iEEE, New York, 1980.
	9	Matthew Hennessy , Robin Milner, On Observing Nondeterminism and Concurrency, Proceedings of the 7th Colloquium on Automata, Languages and Programming, p.299-309, July 14-18, 1980
	10	HENNESS'r, M., AND DE NfCOLA, R,Testing equivalences for processes. In Proceedmgs of the 1983 lnternattonal Conference on Automata, Languages, and Programming (ICALP 83). Lecture Notes in Computer Science, vol. 154. Springer-Verlag, New York, 1983.
	11	Matthew Hennessy , Gordon D. Plotkin, A Term Model for CCS, Proceedings of the 9th Symposium on Mathematical Foundations of Computer Science, p.261-274, September 01-05, 1980
	12	C. A. R. Hoare, Communicating sequential processes, Communications of the ACM, v.21 n.8, p.666-677, Aug. 1978 [doi>10.1145/359576.359585]
	13	HOARE, C. A. R.A model for commumcating sequential processes. Tech. Report PRG-22, Oxford Untv. Programming Research Group, Oxford, England, 1981.
	14	HOARE, C.A.R., BROOKES, S.D., AND ROSCOE, A.W. A theory of communicating sequential processes. Teeh. Report PRG-t6, Oxford Univ. Programming Research Group, Oxford, England, 1981.
	15	KENNAWAY, J.R.Formal semantics of nondeterminism and parallelism, D.Phii, dissertation, Oxford Univ., Oxford, England, 1981.
	16	LAMPORT, L.Proving the correctness of mulfiprocess programs, IEEE Trans. Soflw. Eng. SE-3, 2 (Mar. 1977).
	17	Gary Marc Levin, Proof rules for communicating sequential processes, 1980
	18	Robert Milne , C. Strachey, A Theory of Programming Language Semantics, Halsted Press, New York, NY, 1977
	19	MILNER, R.Algebras for communicating systems. Tech. Report CSR-25-78, Computer Science Dept., Edinburgh Umv., Edinburgh, England, 1978.
	20	R. Milner, A Calculus of Communicating Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
	21	Rocco De Nicola, A Complete Set of Axioms for a Theory of Communicating Sequential Processes, Proceedings of the 1983 International FCT-Conference on Fundamentals of Computation Theory, p.115-126, August 21-27, 1983
	22	PLOTKIN, G.An operational semantics for CSP. In Proceedmgs of the W.G.Z2 Conference, 1982.
	23	RoscoE, A.W.A mathematical theory of commumcating processes. D.Pkil. dissertation, Oxford Umv., Oxford, England, 1982.
	24	ROSCOE, A. W. Denotational Semantics for occam In preparation.
	25	Roum>s, W.C., AND BROOKES, S.D. Possible futures, acceptances, refusals and communicating processes. In Proceedings of the 22nd IEEE Foundations of Computer Science Symposium. IEEE, New York, 1981.
	26	SCOTT, D.S.Data types as latttces. SIAM J Comput. 5 (1976), 522-587.
	27	SMYTH, M.B.Powerdomams. J Comput. Syst. Sct 16 (1978).
	28	STOY, J. E.Denotatmnat Semanttcs MIT Press, Cambridge, Mass., 1977.
	29	ZHou, C.C., AND HOARE, C. A.R. Partial correctness of communicating processes and protocols. Tech. Report PRG-20, Oxford Umv. Programming Research Group, Oxford, England, 1981.

CITED BY 85

	Robert L. Ashenhurst, ACM forum, Communications of the ACM, v.30 n.9, p.752-753, Sept. 1987
	Rance Cleaveland , Scott A. Smolka, Strategic directions in concurrency research, ACM Computing Surveys (CSUR), v.28 n.4, p.607-625, Dec. 1996
	D. G. Weber, Formal specification of fault-tolerance and its relation to computer security, ACM SIGSOFT Software Engineering Notes, v.14 n.3, p.273-277, May 1989
	Ed Brinksma , Holger Hermanns, Process algebra and Markov chains, Lectures on formal methods and performance analysis: first EEF/Euro summer school on trends in computer science, Springer-Verlag New York, Inc., New York, NY, 2002
	Rob J. van Glabbeek , W. Peter Weijland, Branching time and abstraction in bisimulation semantics, Journal of the ACM (JACM), v.43 n.3, p.555-600, May 1996
	Robin Milner, Elements of interaction: Turing award lecture, Communications of the ACM, v.36 n.1, p.78-89, Jan. 1993
	J. Zwiers , W. Roever, Predicates are predicate transformers: a unified compositional theory for concurrency, Proceedings of the eighth annual ACM Symposium on Principles of distributed computing, p.265-279, June 1989, Edmonton, Alberta, Canada
	Vijay A. Saraswat , Martin Rinard, Concurrent constraint programming, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.232-245, December 1989, San Francisco, California, United States
	Shmuel Katz , Gadi Taubenfeld, What processes know: Definitions and proof methods, Proceedings of the fifth annual ACM symposium on Principles of distributed computing, p.249-262, August 11-13, 1986, Calgary, Alberta, Canada
	Ilaria Castellani , Matthew Hennessy, Distributed bisimulations, Journal of the ACM (JACM), v.36 n.4, p.887-911, Oct. 1989
	M. E. Majster-Cederbaum, Underspecification for a simple process algebra of recursive processes, Theoretical Computer Science, v.266 n.1-2, p.935-950, 09/06/2001
	Shing Chi Cheung , Jeff Kramer, Context constraints for compositional reachability analysis, ACM Transactions on Software Engineering and Methodology (TOSEM), v.5 n.4, p.334-377, Oct. 1996
	Rosalie Steier, Authors, Communications of the ACM, v.30 n.9, p.749-ff., Sept. 1987
	Rance Cleaveland , Daniel Yankelevich, An operational framework for value-passing processes, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.326-338, January 16-19, 1994, Portland, Oregon, United States
	Paris C. Kanellakis , Scott A. Smolka, On the analysis of cooperation and antagonism in networks of communicating processes, Proceedings of the fourth annual ACM symposium on Principles of distributed computing, p.23-38, August 1985, Minaki, Ontario, Canada
	Bard Bloom , Sorin Istrail , Albert R. Meyer, Bisimulation can't be traced, Journal of the ACM (JACM), v.42 n.1, p.232-268, Jan. 1995
	Frank S. de Boer , Rogier M. van Eijk , Wiebe van der Hoek , John-Jules Ch. Meyer, A fully abstract model for the exchange of information in multi-agent systems, Theoretical Computer Science, v.290 n.3, p.1753-1773, 3 January 2003
	J. C. M. Baeten , J. A. Bergstra , J. W. Klop, Decidability of bisimulation equivalence for process generating context-free languages, Journal of the ACM (JACM), v.40 n.3, p.653-682, July 1993
	Michal Young , Richard N. Taylor , David L. Levine , Kari A. Nies , Debra Brodbeck, A concurrency analysis tool suite for Ada programs: rationale, design, and preliminary experience, ACM Transactions on Software Engineering and Methodology (TOSEM), v.4 n.1, p.65-106, Jan. 1995
	V. Carchiolo , A. Di Stefano , A. Faro , G. Pappalardo, ECCS and LIPS: two languages for OSI systems specification and verification, ACM Transactions on Programming Languages and Systems (TOPLAS), v.11 n.2, p.284-329, April 1989
	L. Aceto , M. Hennessy, Termination, deadlock, and divergence, Journal of the ACM (JACM), v.39 n.1, p.147-187, Jan. 1992
	Mauro Pezzè , Richard N. Taylor , Michal Young, Graph models for reachability analysis of concurrent programs, ACM Transactions on Software Engineering and Methodology (TOSEM), v.4 n.2, p.171-213, April 1995
	Wei Jen Yeh , Michal Young, Compositional reachability analysis using process algebra, Proceedings of the symposium on Testing, analysis, and verification, p.49-59, October 08-10, 1991, Victoria, British Columbia, Canada
	Pierpaolo Degano , Ugo Montanari, A model for distributed systems based on graph rewriting, Journal of the ACM (JACM), v.34 n.2, p.411-449, April 1987
	B. Bloom , S. Istrail , A. R. Meyer, Bisimulation can't be traced, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.229-239, January 10-13, 1988, San Diego, California, United States
	van Vicious Nguyen , Rob Strom, Process semantics: universal axioms compositional rules, and applications, Proceedings of the seventh annual ACM Symposium on Principles of distributed computing, p.232-247, August 15-17, 1988, Toronto, Ontario, Canada
	Arend Rensink , Roberto Gorrieri, Vertical implementation, Information and Computation, v.170 n.1, p.95-133, October 10, 2001
	Ryszard Janicki, How to relieve a programmer from synchronization details, Proceedings of the 1988 ACM sixteenth annual conference on Computer science, p.438-446, February 1988, Atlanta, Georgia, United States
	Peter Sewell , Jan Vitek, Secure composition of untrusted code: box π, wrappers, and causality types, Journal of Computer Security, v.11 n.2, p.135-187, May 2003
	Paul Gastin , Michael Mislove, A truly concurrent semantics for a process algebra using resource pomsets, Theoretical Computer Science, v.281 n.1-2, p.369-421, June 3 2002
	W. L. Yeung , S. A. Schneider, Design and Verification of Distributed Recovery Blocks with CSP, Formal Methods in System Design, v.22 n.3, p.225-248, May 2003
	Heike Wehrheim, Behavioral Subtyping Relations for Active Objects, Formal Methods in System Design, v.23 n.2, p.143-170, September 2003
	Catuscia Palamidessi, Mobile calculi for distributed programming, Proceedings of the 4th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.74-75, October 06-08, 2002, Pittsburgh, PA, USA
	A. Giacalone , S. A. Smolka, Integrated Environments for Formally Well-Founded Design and Simulation of Concurrent Systems, IEEE Transactions on Software Engineering, v.14 n.6, p.787-802, June 1988
	Oscar Nierstrasz, Regular types for active objects, ACM SIGPLAN Notices, v.28 n.10, p.1-15, Oct. 1, 1993
	M. Hennessy, Acceptance trees, Journal of the ACM (JACM), v.32 n.4, p.896-928, Oct. 1985
	J W de Bakker , J J Meyer , E R Olderog , J I Zucker, Transition systems, infinitary languages and the semantics of uniform concurrency, Proceedings of the seventeenth annual ACM symposium on Theory of computing, p.252-262, May 06-08, 1985, Providence, Rhode Island, United States
	Antti Valmari, Composition and abstraction, Modeling and verification of parallel processes, Springer-Verlag New York, Inc., New York, NY, 2001
	Richard Gerber , Insup Lee, Guest A Layered Approach to Automating the Verification of Real-Time Systems, IEEE Transactions on Software Engineering, v.18 n.9, p.768-784, September 1992
	Graeme Smith , John Derrick, Specification, Refinement and Verification of Concurrent Systems—An Integration of Object-Z and CSP, Formal Methods in System Design, v.18 n.3, p.249-284, May 2001
	M. Notomi , T. Murata, Hierarchical Reachability Graph of Bounded Petri Nets for Concurrent-Software Analysis, IEEE Transactions on Software Engineering, v.20 n.5, p.325-336, May 1994
	Bard Bloom , Wan Fokkink , Rob J. van Glabbeek, Precongruence formats for decorated trace semantics, ACM Transactions on Computational Logic (TOCL), v.5 n.1, p.26-78, January 2004
	Wil Janssen , Mannes Poel , Job Zwiers, The compositional approach to sequential consistency and lazy caching, Distributed Computing, v.12 n.2/3, p.105-127, June 1999
	Ernst-Rüdiger Olderog , Heike Wehrheim, Specification and (property) inheritance in CSP-OZ, Science of Computer Programming, v.55 n.1-3, p.227-257, March 2005
	Bengt Jonsson, A fully abstract trace model for dataflow and asynchronous networks, Distributed Computing, v.7 n.4, p.197-212, May 1994
	Ufuk Celikkan , Rance Cleaveland, Generating diagnostic information for behavioral preorders, Distributed Computing, v.9 n.2, p.61-75, October 1995
	J. C. M. Baeten, A brief history of process algebra, Theoretical Computer Science, v.335 n.2-3, p.131-146, 23 May 2005
	Alan Jeffrey , Julian Rathke, A fully abstract may testing semantics for concurrent objects, Theoretical Computer Science, v.338 n.1-3, p.17-63, 10 June 2005
	S. S. Lam , A. U. Shankar, A Theory of Interfaces and Modules - I: Composition Theorem, IEEE Transactions on Software Engineering, v.20 n.1, p.55-71, January 1994
	A. P. Moore, The Specification and Verified Decomposition of System Requirements Using CSP, IEEE Transactions on Software Engineering, v.16 n.9, p.932-948, September 1990
	Riccardo Focardi , Roberto Gorrieri, The Compositional Security Checker: A Tool for the Verification of Information Flow Security Properties, IEEE Transactions on Software Engineering, v.23 n.9, p.550-571, September 1997
	Markus Lohrey , Pedro R. D'Argenio , Holger Hermanns, Axiomatising divergence, Information and Computation, v.203 n.2, p.115-144, December 15, 2005
	Wan Fokkink , Rob van Glabbeek , Paulien de Wind, Compositionality of Hennessy-Milner logic by structural operational semantics, Theoretical Computer Science, v.354 n.3, p.421-440, 4 April 2006
	J. A. Bergstra , I. Bethke, Polarized process algebra with reactive composition, Theoretical Computer Science, v.343 n.3, p.285-304, 17 October 2005
	Robin Milner, Pure bigraphs: structure and dynamics, Information and Computation, v.204 n.1, p.60-122, January 2006
	Christel Baier , Marjan Sirjani , Farhad Arbab , Jan Rutten, Modeling component connectors in Reo by constraint automata, Science of Computer Programming, v.61 n.2, p.75-113, July 2006
	Rance Cleaveland , S. Purushothaman Iyer , Murali Narasimha, Probabilistic temporal logics via the modal mu-calculus, Theoretical Computer Science, v.342 n.2-3, p.316-350, 7 September 2005
	J. A. Bergstra , C. A. Middelburg, Splitting bisimulations and retrospective conditions, Information and Computation, v.204 n.7, p.1083-1138, July 2006
	Maciej Koutny , Giuseppe Pappalardo, Behaviour Abstraction for Communicating Sequential Processes, Fundamenta Informaticae, v.48 n.1, p.21-54, January 2001
	Vaughan R. Pratt, Transition and cancellation in concurrency and branching time, Mathematical Structures in Computer Science, v.13 n.4, p.485-529, August 2003
	Yuxin Deng , Rob van Glabbeek , Matthew Hennessy , Carroll Morgan , Chenyi Zhang, Remarks on Testing Probabilistic Processes, Electronic Notes in Theoretical Computer Science (ENTCS), 172, p.359-397, April, 2007
	John Derrick , Eerke Boiten, Relational Concurrent Refinement with Internal Operations, Electronic Notes in Theoretical Computer Science (ENTCS), 187, p.35-53, July, 2007
	Kamal Lodaya, A regular viewpoint on processes and algebra, Acta Cybernetica, v.17 n.4, p.751-763, January 2006
	Maurice H. ter Beek , Clarence A. Ellis , Jetty Kleijn , Grzegorz Rozenberg, Team automata for spatial access control, Proceedings of the seventh conference on European Conference on Computer Supported Cooperative Work, p.59-77, September 16-20, 2001, Bonn, Germany
	Gerald Lüttgen , Walter Vogler, Conjunction on processes: Full abstraction via ready-tree semantics, Theoretical Computer Science, v.373 n.1-2, p.19-40, March, 2007
	Arend Rensink , Walter Vogler, Fair testing, Information and Computation, v.205 n.2, p.125-198, February, 2007
	David Basin , Ernst-Ruediger Olderog , Paul E. Sevinc, Specifying and analyzing security automata using CSP-OZ, Proceedings of the 2nd ACM symposium on Information, computer and communications security, March 20-22, 2007, Singapore
	Alban Ponse , Mark B. van der Zwaag, Belnap's logic and conditional composition, Theoretical Computer Science, v.388 n.1-3, p.319-336, December, 2007
	Dipankar Das , P. P. Chakrabarti , Rajeev Kumar, Functional verification of task partitioning for multiprocessor embedded systems, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.12 n.4, p.44-es, September 2007
	Robin Milner, Elements of interaction, ACM Turing award lectures, ACM, New York, NY, 2007
	James J. Leifer , Robin Milner, Transition systems, link graphs and Petri nets, Mathematical Structures in Computer Science, v.16 n.6, p.989-1047, December 2006
	J. A. Bergstra , C. A. Middelburg, Thread Algebra with Multi-Level Strategies, Fundamenta Informaticae, v.71 n.2,3, p.153-182, August 2006
	Oscar Nierstrasz , Michael Papathomas, Towards a type theory for active objects, ACM SIGPLAN OOPS Messenger, v.2 n.2, p.89-93, Apr. 1991
	H. von Issendorff, A theory of organization, ACM SIGPLAN Notices, v.25 n.9, p.31-38, Sep. 1990
	Supratik Bose , Siddhartha Mukhopadhyay , Amit Patra, A Nondeterministic Extension over Finitely Recursive ProcessModel, Discrete Event Dynamic Systems, v.7 n.3, p.243-274, June 1997
	H. Von Issendorff, A theory of organization, ACM SIGPLAN Notices, v.25 n.8, p.84-102, Aug. 1990
	Gul A. Agha , Ian A. Mason , Scott F. Smith , Carolyn L. Talcott, A foundation for actor computation, Journal of Functional Programming, v.7 n.1, p.1-72, January 1997
	Jayasri Banerjee , Anup Kumar Bandyopadhyay , Ajit Kumar Mandal, Application of Dijkstra's weakest precondition calculus to Dining Philosophers problem, ACM SIGSOFT Software Engineering Notes, v.32 n.4, July 2007
	Alan Jeffrey , Julian Rathke, Full abstraction for polymorphic π-calculus, Theoretical Computer Science, v.390 n.2-3, p.171-196, January, 2008
	J. a. Bergstra , C. a. Middelburg, Maurer computers for pipelined instruction processing†, Mathematical Structures in Computer Science, v.18 n.2, p.373-409, April 2008
	Taolue Chen , Wan Fokkink , Rob van Glabbeek, Ready to preorder: The case of weak process semantics, Information Processing Letters, v.109 n.2, p.104-111, December, 2008
	Jos c. m. Baeten , Mario Bravetti, A ground-complete axiomatisation of finite-state processes in a generic process algebra, Mathematical Structures in Computer Science, v.18 n.6, p.1057-1089, December 2008
	Irek Ulidowski , Shoji Yuen, Generating priority rewrite systems for OSOS process languages, Information and Computation, v.207 n.2, p.120-145, February, 2009
	Rob van Glabbeek , Ursula Goltz , Jens-Wolfhard Schicke, Symmetric and Asymmetric Asynchronous Interaction, Electronic Notes in Theoretical Computer Science (ENTCS), v.229 n.3, p.77-95, July, 2009
	Patrick H. S. Brito , Rogério De Lemos , Cecília M. F. Rubira , Eliane Martins, Architecting fault tolerance with exception handling: verification and validation, Journal of Computer Science and Technology, v.24 n.2, p.212-237, March 2009

INDEX TERMS

Primary Classification:
F. Theory of Computation
F.3 LOGICS AND MEANINGS OF PROGRAMS

Additional Classification:
D. Software
D.1 PROGRAMMING TECHNIQUES
D.3 PROGRAMMING LANGUAGES
D.3.1 Formal Definitions and Theory
Subjects: Semantics
D.3.2 Language Classifications

Nouns: CSP

General Terms:
Theory

REVIEW

"A. Prasad Sistla : Reviewer"

Giving precise and well-defined meanings to programs and programming languages allows implementors of programming languages to prove the correctness of their implementations with respect to their specifications. For sequential programs, the me more...

Collaborative Colleagues:

S. D. Brookes: colleagues

C. A. R. Hoare: colleagues

A. W. Roscoe: colleagues

Adobe Acrobat

QuickTime

Windows Media Player

Real Player