A Proof System for Communicating Sequential Processes

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A Proof System for Communicating Sequential Processes

Full text

Pdf (1.57 MB)

Source

ACM Transactions on Programming Languages and Systems (TOPLAS) archive
Volume 2 , Issue 3 (July 1980) table of contents

Pages: 359 - 385

Year of Publication: 1980

ISSN:0164-0925

Authors

Krzysztof R. Apt	Faculty of Economics, University of Rotterdam, P.O. Box 1738, 3000 DR Rotterdam, The Netherlands
Nissim Francez	Department of Computer Science, Technion-Israel Institute of Technology, Haifa, Israel and Department of Computer Science, University of Utrecht, P.O. Box 80.002, 3508 TA Utrecht, The Netherlands
Willem P. de Roever	Department of Computer Science, Technion-Israel Institute of Technology, Haifa, Israel and Department of Computer Science, University of Utrecht, P.O. Box 80.002, 3508 TA Utrecht, The Netherlands

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 10, Downloads (12 Months): 65, Citation Count: 69

Additional Information:

abstract references cited by index terms 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/357103.357110 What is a DOI?

ABSTRACT

An axiomatic proof system is presented for proving partial correctness and absence of deadlock (and failure) of communicating sequential processes. The key (meta) rule introduces cooperation between proofs, a new concept needed to deal with proofs about synchronization by message passing. CSP's new convention for distributed termination of loops is dealt with. Applications of the method involve correctness proofs for two algorithms, one for distributed partitioning of sets, the other for distributed computation of the greatest common divisor of n numbers.

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	APT, K.R. Recursive assertions and parallel programs. Submitted for publication.
	2	APT, K.R., DE ROEVER, W.P., AND FRANCEZ, N. Weakest precondition semantics for communicaring processes. To appear.
	3	ASHCRO~r, E. Proving assertions about parallel programs. J. Comput. Syst. Sci. 10 (1975), 110- 135.
	4	K. M Chandy , Jayadev Misra, An Axiomatic Proof Technique for Networks of Communicating Processes, University of Texas at Austin, Austin, TX, 1979
	5	DIJKSTRA, E.W. A correctness proof for communicating processes--A small exercise. EWD-607, Burroughs, Nuenen, The Netherlands, 1977.
	6	Nissim Francez, Distributed Termination, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.1, p.42-55, Jan. 1980 [doi>10.1145/357084.357087]
	7	FRANCEZ, N., HOARE, C.A.R., LEHMANN, D.J., AND DE ROEVER, W.P. Semantics of nondeterminism, concurrency and communication. J. Comput. Syst. Sci. 19 (1979), 290-308.
	8	FRANCEZ, N., AND PNUELI, A. A proof method for cyclic programs. Acta Inf. 9 (1978).
	9	FRANCEZ, N., AND RODEH, M. Achieving distributed termination without freezing. Rep. TR 72, IBM Israel Scientific Center, 1980.
	10	HOARE, C.A.R. Towards a theory of parallel programming. In Operating Systems Techniques, C.A.R. Hoare and R. Perrot, Eds., Academic Press, New York, 1972.
	11	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]
	12	John H. Howard, Proving monitors, Communications of the ACM, v.19 n.5, p.273-279, May 1976 [doi>10.1145/360051.360079]
	13	LAMPORT, L. Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 3, 2 (1977), 125-143.
	14	Gary M Levin, Proof Rules for Communicating Sequential Processes, Cornell University, Ithaca, NY, 1980
	15	MAZVRKIEWICZ, A. A complete set of assertions on distributed systems. Inst. of Computer Science, Polish Academy of Science, 1979.
	16	Susan Owicki, A consistent and complete deductive system for the verification of parallel programs, Proceedings of the eighth annual ACM symposium on Theory of computing, p.73-86, May 03-05, 1976, Hershey, Pennsylvania, United States [doi>10.1145/800113.803634]
	17	Susan Owicki , David Gries, Verifying properties of parallel programs: an axiomatic approach, Communications of the ACM, v.19 n.5, p.279-285, May 1976 [doi>10.1145/360051.360224]
	18	OWlCKI, S.S., AND GRIES, D. An axiomatic proof technique for parallel programs. L Acta Inf. 6, 1976, 319-340.

CITED BY 69

	Rogier M. Van Eijk , Frank S. De Boer , Wiebe Van Der Hoek , John-Jules Ch. Meyer, A Verification Framework for Agent Communication, Autonomous Agents and Multi-Agent Systems, v.6 n.2, p.185-219, March 2003
	Laura K. Dillon, Using symbolic execution for verification of Ada tasking programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.12 n.4, p.643-669, Oct. 1990
	John Howard , Shmuel Katz, Reconciliations, Proceedings of the thirteenth annual ACM symposium on Principles of distributed computing, p.14-21, August 14-17, 1994, Los Angeles, California, United States
	George S. Avrunin , Jack C. Wileden, Describing and analyzing distributed software system designs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.3, p.380-403, July 1985
	J. Misra , K. M. Chandy , Todd Smith, Proving safety and liveness of communicating processes with examples, Proceedings of the first ACM SIGACT-SIGOPS symposium on Principles of distributed computing, p.201-208, August 18-20, 1982, Ottawa, Canada
	Yuh-Jzer Joung , Scott A. Smolka, A comprehensive study of the complexity of multiparty interaction, Journal of the ACM (JACM), v.43 n.1, p.75-115, Jan. 1996
	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
	Shimon Cohen , Daniel Lehmann, Dynamic systems and their distributed termination, Proceedings of the first ACM SIGACT-SIGOPS symposium on Principles of distributed computing, p.29-33, August 18-20, 1982, Ottawa, Canada
	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
	G. N. Buckley , Abraham Silberschatz, An Effective Implementation for the Generalized Input-Output Construct of CSP, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.2, p.223-235, April 1983
	Valérie Issarny, An exception handling model for parallel programming and its verification, ACM SIGSOFT Software Engineering Notes, v.16 n.5, p.92-100, Dec. 1991
	Krzysztof R. Apt, Formal Justification of a Proof System for Communicating Sequential Processes, Journal of the ACM (JACM), v.30 n.1, p.197-216, Jan. 1983
	Frank S. de Boer , Maurizio Gabbrielli , Elena Marchiori , Catuscia Palamidessi, Proving concurrent constraint programs correct, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.98-108, January 16-19, 1994, Portland, Oregon, United States
	Werner Damm, An axiomatization of low-level parallelism in microarchitectures, ACM SIGMICRO Newsletter, v.15 n.4, p.314-323, Dec. 1984
	Leslie Lamport , Fred B. Schneider, The ``Hoare Logic'' of CSP, and All That, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.2, p.281-296, April 1984
	J. Widom , D. Gries , F. B. Schneider, Completeness and incompleteness of trace-based network proof systems, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.27-38, January 21-23, 1987, Munich, West Germany
	Gregory R. Andrews , Fred B. Schneider, Concepts and Notations for Concurrent Programming, ACM Computing Surveys (CSUR), v.15 n.1, p.3-43, March 1983
	Laura K. Dillon, Verifying General Safety Properties of Ada Tasking Programs, IEEE Transactions on Software Engineering, v.16 n.1, p.51-63, January 1990
	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
	Richard D. Schlichting , Fred B. Schneider, Understanding and using asynchronous message passing (Preliminary Version), Proceedings of the first ACM SIGACT-SIGOPS symposium on Principles of distributed computing, p.141-147, August 18-20, 1982, Ottawa, Canada
	Abha Moitra, Synthesis of communicating processes, Proceedings of the second annual ACM symposium on Principles of distributed computing, p.123-130, August 17-19, 1983, Montreal, Quebec, Canada
	Orna Grumberg , Nissim Francez , Shmuel Katz, Fair termination of communicating processes, Proceedings of the third annual ACM symposium on Principles of distributed computing, p.254-265, August 27-29, 1984, Vancouver, British Columbia, Canada
	Frédéric Herbreteau , Franck Cassez , Olivier Roux, Application of Partial-Order Methods to Reactive Programswith Event Memorization, Real-Time Systems, v.20 n.3, p.287-316, May 2001
	M. P. Herlihy , J. M. Wing, Axioms for concurrent objects, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.13-26, January 21-23, 1987, Munich, West Germany
	Laura K. Dillon, Task dependence and termination in Ada, ACM Transactions on Software Engineering and Methodology (TOSEM), v.6 n.1, p.80-110, Jan. 1997
	Shmuel Katz , Doron Peled, Interleaving set temporal logic, Proceedings of the sixth annual ACM Symposium on Principles of distributed computing, p.178-190, August 10-12, 1987, Vancouver, British Columbia, Canada
	Howard Barringer , Ruurd Kuiper , Amir Pnueli, Now you may compose temporal logic specifications, Proceedings of the sixteenth annual ACM symposium on Theory of computing, p.51-63, December 1984
	Joylyn Reed , Raymond T. Yeh, Specification and verification of liveness properties of cyclic, concurrent processes, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.1, p.156-177, Jan. 1988
	Jacek Olszewski, CSP laboratory, ACM SIGCSE Bulletin, v.25 n.1, p.91-95, March 1993
	Gregory R. Andrews, Parallel programs: proofs, principles, and practice, Communications of the ACM, v.24 n.3, p.140-145, March 1981
	Huai-An Lin , Ming T. Liu , Charles J. Graff, Verification of a methodology for designing reliable communication protocols, ACM SIGCOMM Computer Communication Review, v.13 n.4, p.141-149, October 1983
	Richard D. Schlichting , Fred B. Schneider, Using message passing for distributed programming: proof rules and disciplines, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.3, p.402-431, July 1984
	Abha Moitra, Technical Correspondence: On Apt, Francez, and de Roever's ``A Proof System for Communicating Sequential Processes'', ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.3, p.500-501, July 1983
	N Liu , M T Liu, Conformity analysis for communication protocols, ACM SIGCOMM Computer Communication Review, v.16 n.3, p.216-226, Aug. 5, 1986
	Maurice P. Herlihy , Jeannette M. Wing, Linearizability: a correctness condition for concurrent objects, ACM Transactions on Programming Languages and Systems (TOPLAS), v.12 n.3, p.463-492, July 1990
	W. Damm, A Microprogramming Logic, IEEE Transactions on Software Engineering, v.14 n.5, p.559-574, May 1988
	Krithivasan Ramamritham, Resource controller tasks in ADA: Their structure and semantics, Proceedings of the 7th international conference on Software engineering, p.67-76, March 26-29, 1984, Orlando, Florida, United States
	G-C. Roman, Specifying software/hardware interactions in distributed systems, Proceedings of the 9th international conference on Software Engineering, p.126-139, March 1987, Monterey, California, United States
	Marty Ossefort, Correctness Proofs of Communicating Processes: Three Illustrative Examples From the Literature, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.4, p.620-640, Oct. 1983
	Nissim Francez, Extended naming conventions for communicating processes, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.40-45, January 25-27, 1982, Albuquerque, Mexico
	Gruia-Catalin Roman , Mark S. Day, Multifaceted distributed systems specification using processes and event synchronization, Proceedings of the 7th international conference on Software engineering, p.44-55, March 26-29, 1984, Orlando, Florida, United States
	S. D. Brookes , C. A. R. Hoare , A. W. Roscoe, A Theory of Communicating Sequential Processes, Journal of the ACM (JACM), v.31 n.3, p.560-599, July 1984
	Krzysztof R. Apt, Correctness proofs of distributed termination algorithms, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.3, p.388-405, July 1986
	Frank S. De Boer , Maurizio Gabbrielli , Elena Marchiori , Catuscia Palamidessi, Proving concurrent constraint programs correct, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.5, p.685-725, Sept. 1997
	Gregory R. Andrews, Synchronizing Resources, ACM Transactions on Programming Languages and Systems (TOPLAS), v.3 n.4, p.405-430, Oct. 1981
	Arthur Bernstein , Paul K. Harter, Jr., Proving real-time properties of programs with temporal logic, ACM SIGOPS Operating Systems Review, v.15 n.5, p.1-11, December 1981
	Jeannette M. Wing, A Specifier's Introduction to Formal Methods, Computer, v.23 n.9, p.8-23, September 1990
	Rob Strom , Shaula Yemini, The NIL distributed systems programming language: a status report, ACM SIGPLAN Notices, v.20 n.5, May 1985
	Christos N. Nikolaou , Edmund M. Clarke , Nissim Francez , Stephen A. Schuman, A methodology for verifying request processing protocols, ACM SIGCOMM Computer Communication Review, v.13 n.2, April 1983
	Franklyn T. Bradshaw , George W. Ernst , Raymond J. Hookway, Use of data abstraction in process specification, ACM SIGSOFT Software Engineering Notes, v.7 n.3, p.16-21, July 1982
	M. van Hulst , J.-J. Ch. Meyer, An epistemic proof system for parallel processes: extended abstract, Proceedings of the 5th conference on Theoretical aspects of reasoning about knowledge, p.243-254, March 13-16, 1994, Pacific Grove, California
	J. M. Adams , A. P. Black, On proof rules for monitors, ACM SIGOPS Operating Systems Review, v.16 n.2, p.18-27, April 1982
	Shlomi Dolev , Frank Stomp, Safety assurance via on-line monitoring, Distributed Computing, v.16 n.4, p.269-277, December 2003
	Shmuel Katz , Doron Peled, Verification of distributed programs using representative interleaving sequences, Distributed Computing, v.6 n.2, p.107-120, September 1992
	Sigurd Meldal, A complete axiomatic semantics of spawning, Distributed Computing, v.5 n.3, p.159-174, December 1991
	Paritosh K. Pandya , Mathai Joseph, P-A logic: a compositional proof system for distributed programs, Distributed Computing, v.5 n.1, p.37-54, June 1991
	Awadhesh Kumar Singh , Anup Kumar Bandyopadhyay, Verifying mutual exclusion and liveness properties with split preconditions, Journal of Computer Science and Technology, v.19 n.6, p.795-802, November 2004
	Jan Peleska, Design and verification of fault tolerant systems with CSP, Distributed Computing, v.5 n.2, p.95-106, September 1991
	J. C. M. Baeten, A brief history of process algebra, Theoretical Computer Science, v.335 n.2-3, p.131-146, 23 May 2005
	Sylvie Damy , Guy-René Perrin, Techniques for the design of communicating processes, Proceedings of the 6th international workshop on Software specification and design, October 25-26, 1991, Como, Italy
	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
	Cees Pierik , Frank S. de Boer, A proof outline logic for object-oriented programming, Theoretical Computer Science, v.343 n.3, p.413-442, 17 October 2005
	K. Culik, On formal and informal proofs for program correctness, ACM SIGPLAN Notices, v.18 n.1, p.23-28, January 1983
	C. B. Jones, Tentative steps toward a development method for interfering programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.4, p.596-619, Oct. 1983
	Krzysztof R. Apt , Nissim Francez, Modeling the distributed termination convention of CSP, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.3, p.370-379, July 1984
	N. Soundararajan, Axiomatic semantics of communicating sequential processes, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.4, p.647-662, Oct. 1984
	Erika Ábrahám , Frank S. de Boer , Willem-Paul de Roever , Martin Steffen, An assertion-based proof system for multithreaded Java, Theoretical Computer Science, v.331 n.2-3, p.251-290, 25 February 2005
	Erika Ábrahám , Frank S. de Boer , Willem-Paul de Roever , Martin Steffen, A Deductive Proof System for Multithreaded Java with Exceptions, Fundamenta Informaticae, v.82 n.4, p.391-463, February 2008
	F. S. de Boer, A shared-variable concurrency analysis of multi-threaded object-oriented programs, Theoretical Computer Science, v.410 n.2-3, p.128-141, February, 2009