Abstract
Proofsystems for proving partial correctness of distributed processes which communicate through message-passing are discussed, using CSP as programming language. Of these the methods due to Levin & Gries [LG]; Apt, Francez & de Roever [AFR]; Lamport & Schneider [LS]; Soundararajan & Dahl [SD]; Zwiers, de Roever & van Emde Boas [ZRE] and Misra & Chandy [MC] are treated in detail (in that order). The main emphasis is the development from a-posteriori verification ([LG],[AFR]) to verification as part of the program design process ([SD],[ZRE],[MC]). New is that, in order to illustrate this development, attempts are made to extend the systems due to [AFR] and [SD] with nested parallelism and hiding.
This paper represents the master's thesis of Jozef Hooman, supervised by Willem-P. de Roever, for obtaining a degree at the University of Nijmegen.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
A. References
Apt, K.R., Ten Years of Hoare's Logic — Part I, Toplas 3 (1981), 431–484.
Apt, K.R., Formal Justification of a proof system for Communicating Sequential Processes, JACM 30 (1983), 197–216.
Apt, K.R., Proving correctness of CSP Programs-a tutorial, Technical report 84-24, LITP, Université Paris 7 (1984).
Apt, K.R. and Francez, N., Modeling the Distributed Termination Convention of CSP, Toplas 6 (1984), 370–379.
Apt, K.R., Francez, N. and de Roever, W.P., A proof system for Communicating Sequential Processes, Toplas 2 (1980), 359–385.
Zhou Chao Chen and Hoare, C.A.R., Partial correctness of CSP, IEEE Int. Conf. on Dist. Comp. Systems (1981).
Floyd, R.W., Assigning meanings to programs, Proc AMS (1967).
Gerth, R.T., Transition logic: how to reason about temporal properties in a compositional way, Proc. STOC (1984).
Hoare, C.A.R., Communicating Sequential Processes, CACM 21 (1978), 666–677.
Hooman, J. and Zwiers, J., Combining sequential and parallel composition: unexpected implications for compositional proofsystems, to appear.
Lamport, L., The "Hoare Logic" of Concurrent Programs, Acta Informatica 14 (1980), 21–37.
Lamport, L., Specifying concurrent program modules, Toplas 5 (1983), 190–223.
Lamport, L. and Schneider, F.B., The "Hoare Logic" of CSP, and all that, Toplas 6 (1984), 281–296.
Levin, G.M., Proofrules for Communicating Sequential Processes, Ph.D.Thesis (1980), TR 80-435, Dept. Comp. Science, Cornell University.
Levin, G.M. and Gries, D., A proof technique for Communicating Sequential Processes, Acta Informatica 15 (1981), 281–302.
Misra, J. and Chandy, K.M., Proofs of Networks of Processes, IEEE Transactions on Software Engineering, SE-7 (1981), 417–426.
Owicki, S.S. and Gries, D., An axiomatic proof technique for parallel programs, Acta informatica 6 (1976), 319–340.
de Roever, W.P., The quest for compositionality — a survey of assertion-based proof systems for concurrent programs, Part I: Concurrency based on shared variables, to appear in: Proc. of the IFIP Working Conference 1985: "The role of abstract models in computer science", E.J. Neuhold (Ed.), North-Holland; also as Technical Report, Univ. of Utrecht (1985).
Soundararajan, N., Axiomatic semantics of Communicating Sequential Processes, Toplas 6 (1984), 647–662.
Soundararajan, N. and Dahl, O.J., Partial correctness semantics for Communicating Sequential Processes, Res. Rep. 66 (1982), Institute for Informatics, Univ. of Oslo, Norway.
Zwiers, J., de Bruin, A. and de Roever, W.P., A proof system for partial correctness of dynamic networks, LNCS 164 (1983).
Zwiers, J., de Roever, W.P. and van Emde Boas, P., Compositionality and concurrent networks: soundness and completeness of a proofsystem, Report no. 57, University of Nijmegen, (1984).
Zwiers, J., de Roever, W.P. and van Emde Boas, P., Compositionality and concurrent networks: soundness and completeness of a proofsystem, to appear in ICALP (1985).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1986 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Hooman, J., de Roever, WP. (1986). The quest goes on: A survey of proofsystems for partial correctness of CSP. In: de Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds) Current Trends in Concurrency. Lecture Notes in Computer Science, vol 224. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0027044
Download citation
DOI: https://doi.org/10.1007/BFb0027044
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-16488-3
Online ISBN: 978-3-540-39827-1
eBook Packages: Springer Book Archive