Axiomatic semantics of communicating sequential processes

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Axiomatic semantics of communicating sequential processes

Full text

Pdf (894 KB)

Source

ACM Transactions on Programming Languages and Systems (TOPLAS) archive
Volume 6 , Issue 4 (October 1984) table of contents
Lecture notes in computer science Vol. 174

Pages: 647 - 662

Year of Publication: 1984

ISSN:0164-0925

Author

N. Soundararajan

The Ohio State Univ.

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 7, Downloads (12 Months): 47, Citation Count: 12

Additional Information:

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/1780.1805 What is a DOI?

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, Formal Justification of a Proof System for Communicating Sequential Processes, Journal of the ACM (JACM), v.30 n.1, p.197-216, Jan. 1983 [doi>10.1145/322358.322372]
	2	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]
	3	DAHL, O.J. Can program proving be made practical? Res. Pep. 33, Institute for Informatics, Univ. of Oslo, Norway, 1978.
	4	DIJKSTRA, E.W. A correctness proof for networks of communicating processes--A small exercise, EWD-607. Burroughs, The Netherlands, 1977.
	5	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]
	6	LEVIN, G., AND GmES, D. A proof technique for communicating sequential processes. Acta In{. 15 (1981), 281-302.
	7	MISRA, J., AND CHANDY, K.M. Proofs of networks of processes. }EEE Trans. Softw. Eng. 7 (1981), 417-426.
	8	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]
	9	SOUNDARARAJAN, N. Axiomatic semantics of communicating sequential processes. Res. Pep. 56, Institute for Informatics, Univ. of Oslo, Norway, 1981.
	10	SOUNDARARAJAN, N. Correctness proofs of CSP programs. Res. Pep. 59, Institute for Informatics, Univ. of Oslo, Norway, 1981.
	11	SOUNDARARAJAN, N., AND DAHL, O.J. Partial correctness semantics for communicating sequential processes. Pes. Pep. 66, Institute for Informatics, Univ. of Oslo, Norway, 1982.

CITED BY 12

	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
	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
	Neelam Soundarajan, Documenting framework behavior, ACM Computing Surveys (CSUR), v.32 n.1es, March 2000
	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
	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
	Leo Yuhsiang Liu , R. K. Shyamasundar, Static Analysis of Real-Time Distributed Systems, IEEE Transactions on Software Engineering, v.16 n.4, p.373-388, April 1990
	A. K. Elmagarmid , N. Soundararajan , M. T. Liu, A Distributed Deadlock Detection and Resolution Algorithm and its Correctness Proof, IEEE Transactions on Software Engineering, v.14 n.10, p.1443-1452, October 1988
	Steve Carr , Changpeng Fang , Tim Jozwowski , Jean Mayo , Ching-Kuang Shene, A communication library to support concurrent programming courses, ACM SIGCSE Bulletin, v.34 n.1, March 2002
	Yingzhou Zhang , Baowen Xu, A survey of semantic description frameworks for programming languages, ACM SIGPLAN Notices, v.39 n.3, March 2004
	Marcel kyas , Frank S. de Boer , Willem-paul de Roever, A compositional trace logic for behavioural interface specifications, Nordic Journal of Computing, v.12 n.2, p.116-132, August 2005
	Ahmed K. Elmagarmid, A survey of distributed deadlock detection algorithms, ACM SIGMOD Record, v.15 n.3, p.37-45, Sept. 1986
	Johan Dovland , Einar Broch Johnsen , Olaf Owe, Observable Behavior of Dynamic Systems: Component Reasoning for Concurrent Objects, Electronic Notes in Theoretical Computer Science (ENTCS), v.203 n.3, p.19-34, May, 2008

INDEX TERMS

Classification:
D. Software
D.1 PROGRAMMING TECHNIQUES
D.1.3 Concurrent Programming

Nouns: CSP
D.2 SOFTWARE ENGINEERING
D.2.4 Software/Program Verification
Subjects: Correctness proofs
D.3 PROGRAMMING LANGUAGES
D.3.3 Language Constructs and Features
Subjects: Concurrent programming structures
D.4 OPERATING SYSTEMS
D.4.1 Process Management
Subjects: Deadlocks

F. Theory of Computation
F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Languages, Verification

REVIEW

"Kamal Lodaya : Reviewer"

The author gives a proof system for CSP that involves the following procedures: (1)Prove the correctness of the individual processes of a CSP program in isolation from other processes. Assertions used i more...

Collaborative Colleagues:

N. Soundararajan: colleagues

Adobe Acrobat

QuickTime

Windows Media Player

Real Player