×

Correctness of concurrent processes. (English) Zbl 0745.68045

Summary: A new notion of correctness for concurrent processes is introduced and investigated. It is a relationship \(P sat S\) between process terms \(P\) built up from operators of CCS by R. Milner [A calculus of communicating systems. Berlin etc.: Springer-Verlag, 171 p. (1980; Zbl 0452.68027)], CSP by C. A. R. Hoare [Communicating sequential processes. Englewood Cliffs/NJ etc.: Prentice-Hall Int., 256 p. (1985; Zbl 0637.68007)] and COSY by P. E. Lauer, P. R. Torrigiani and M. W. Shields [Acta Inf. 12, 109-158 (1979; Zbl 0403.68031)] and logical formulas \(S\) specifying sets of finite communication sequences. The definition of \(P sat S\) is based on Petri net semantics for process terms by E. R. Olderog [Lect. Notes Comput. Sci. 354, No. 16, 549-573 (1989; Zbl 0683.68070)]. The main point is that \(P sat S\) requires a simple liveness property of the net denoted by \(P\). This implies that \(P\) is divergence free and externally deterministic. Process correctness \(P sat S\) determines a new semantic model for process terms and logical formulas. It is a modification \({\mathfrak R}^*\) of the readiness semantics [E. R. Olderog and T. Hoare, Acta Inf. 23, 9-66 (1986; Zbl 0582.68008) (preview Zbl 0569.68019)] which is fully abstract with respect to the relation \(P sat S\). The model \({\mathfrak R}^*\) abstracts from the concurrent behaviour of process terms and certain aspects of their internal activity. In \({\mathfrak R}^*\) process correctness \(P sat S\) boils down to semantic equality: \({\mathfrak R}^*[[P]]={\mathfrak R}^*[[S]]\). The modified readiness equivalence is closely related to failure equivalence by S. D. Brookes, C. A. R. Hoare and A. W. Roscoe [J. Assoc. Comput. Mach. 31, 560-599 (1984; Zbl 0628.68025)] and strong testing equivalence by R. De Nicola and M. Hennessy [Testing equivalences for processes, Theor. Comput. Sci. 34, 83-134 (1984)].

MSC:

68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
68Q55 Semantics in the theory of computing

Software:

COSY
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Astesiano, E., Combining an operational with an algebraic approach to the specification of concurrency, (Bjørner, D., Proc. Workshop on Combining Methods (1984), Nyborg: Nyborg Denmark)
[2] Alpern, B.; Schneider, F. B., Defining liveness, Inform. Process. Lett., 21, 181-185 (1985) · Zbl 0575.68030
[3] de Bakker, J. W.; Meyer, J.-J.; Olderog, E.-R.; Zucker, J. I., Transition systems, metric spaces and ready sets in the semantics of uniform concurrency, J. Comput. System Sci., 36, 158-224 (1988) · Zbl 0652.68028
[4] Best, E., COSY: its relation to nets and CSP, (Brauer, W.; Reisig, W.; Rozenberg, G., Petri Nets: Applications and Relationships to Other Models of Concurrency. Petri Nets: Applications and Relationships to Other Models of Concurrency, Lecture Notes in Computer Science, 255 (1987), Springer: Springer Berlin), 416-440 · Zbl 0626.68025
[5] Bergstra, J. A.; Klop, J. W.; Olderog, E.-R., Failures without chaos: a new process semantics for fair abstraction, (Wirsing, M., Proc. IFIP Working Conf. on Formal Description of Programming Concepts III (1987), North-Holland: North-Holland Amsterdam), 77-101
[6] Bretschneider, M.; Duque Antón, M.; Fink, A., Constructing and verifying protocols using TCSP, (Aggarwal, S.; Sabnani, K., Proc. IFIP Working Conf. on Protocol Specification, Testing and Verification (1988), North-Holland: North-Holland Amsterdam)
[7] Brookes, S. D.; Hoare, C. A.R.; Roscoe, A. W., A theory of communicating sequential processes, J. ACM, 31, 560-599 (1984) · Zbl 0628.68025
[8] Chaochen, Z.; Hoare, C. A.R., Partial correctness of communicating processes, Proc. 2nd Internat. Conf. on Distributed Comput. Systems (1981), Paris
[9] DeNicola, R.; Hennessy, M., Testing equivalences for processes, Theoret. Comput. Sci., 34, 83-134 (1984) · Zbl 0985.68518
[10] Dijkstra, E. W., A Discipline of Programming (1976), Prentice Hall: Prentice Hall Englewood Cliffs, NJ · Zbl 0286.00013
[11] Duque Antón, M.; Bretschneider, M., Formulas, processes and Petri-nets applied to the specification and verification of a HDLC protocol, (Diaz, J.; Orejas, F., Proc. TAPSOFT ’89. Proc. TAPSOFT ’89, Vol. 2, Lecture Notes in Computer Science, 352 (1989), Springer: Springer Berlin), 140-154
[12] Francez, N.; Lehmann, D.; Pnueli, A., A linear history semantics for languages for distributed programming, Theoret. Comput. Sci., 32, 25-46 (1984) · Zbl 0543.68019
[13] Goltz, U., Über die Darstellung von CCS-Programmen durch Petrinetze, (Doctoral Diss. (1988), RWTH: RWTH Aachen)
[14] Hennessy, M., Algebraic Theory of Processes (1988), MIT Press: MIT Press Cambridge, MA · Zbl 0744.68047
[15] Hennessy, M.; Plotkin, G. D., Full abstraction for a simple programming language, (Becvar, J., 8th Symp. on Math. Found. of Comput. Sci.. 8th Symp. on Math. Found. of Comput. Sci., Lecture Notes in Computer Science, 74 (1979), Springer: Springer Berlin), 108-120 · Zbl 0457.68006
[16] Hoare, C. A.R., Some properties of predicate transformers, J. ACM, 25, 461-480 (1978) · Zbl 0379.68016
[17] Hoare, C. A.R., A calculus of total correctness for communicating processes, Sci. Comput. Progr., 1, 44-72 (1981) · Zbl 0485.68025
[18] Hoare, C. A.R., Communicating Sequential Processes (1985), Prentice Hall: Prentice Hall London · Zbl 0637.68007
[19] Jonsson, B., Compositional verification of distributed systems, (Ph.D. Thesis (1987), Dept. Comput. Sci., Uppsala Univ)
[20] Lauer, P. E.; Torrigiani, P. R.; Shields, M. W., COSY—A system specification language based on paths and processes, Acta Inform., 12, 109-158 (1979) · Zbl 0403.68031
[21] Mazurkiewicz, A., Concurrent program schemes and their interpretations, (Tech. Report DAIMI PB-78 (1977), Aarhus Univ)
[22] Meyer, A. R.; Sieber, K., Towards fully abstract semantics for local variables, Preliminary Report, Proc. 15th ACM Symp. Principles of Program. Lang., 191-203 (1988), San Diego, CA
[23] Milner, R., Fully abstract models of typed A-calculi, Theoret. Comput. Sci., 4, 1-22 (1977) · Zbl 0386.03006
[24] Milner, R., A Calculus of Communicating Systems, (Lecture Notes in Computer Science, 92 (1980), Springer: Springer Berlin) · Zbl 0452.68027
[25] Misra, J.; Chandy, K. M., Proofs of networks of processes, IEEE Trans. Software Eng., 7, 417-426 (1981) · Zbl 0468.68030
[26] Olderog, E.-R., Nets, terms and formulas: three views of concurrent processes and their relationship, Habilitationsschrift, Univ. Kiel (1988/1989), Cambridge University Press, to appear
[27] Olderog, E.-R., Strong bisimilarity on nets: a new concept for comparing net semantics, (de Bakker, J. W.; de Roever, W. P.; Rozenberg, G., Linear Time/Branching Time/Partial Order in the Semantics of Concurrency. Linear Time/Branching Time/Partial Order in the Semantics of Concurrency, Lecture Notes in Computer Science, 354 (1989), Springer: Springer Berlin), 549-573 · Zbl 0683.68070
[28] Olderog, E.-R.; Hoare, C. A.R., Specification-oriented semantics for communicating processes, Acta Inform., 23, 9-66 (1986) · Zbl 0569.68019
[29] Ossefort, M., Correctness proofs of communicating processes: three illustrative examples from the literature, ACM TOPLAS, 5, 620-640 (1983) · Zbl 0517.68054
[30] Owicki, S.; Lamport, L., Proving liveness properties of concurrent programs, ACM TOPLAS, 4, 199-223 (1982) · Zbl 0483.68013
[31] Plotkin, G. D., LCF considered as a programming language, Theoret. Comput. Sci., 5, 223-255 (1977) · Zbl 0369.68006
[32] Reisig, W., Petri nets, an introduction, (EATCS Monographs on Theoret. Comput. Sci. (1985), Springer: Springer Berlin) · Zbl 0521.68057
[33] Rem, M., Trace theory and systolic computation, (de Bakker, J. W.; Nijman, A. J.; Treleaven, P. C., Proc. PARLE. Conf.. Proc. PARLE. Conf., Vol. I, Lecture Notes in Comput. Sci., 258 (1987), Springer: Springer Berlin), 14-33, Eindhoven
[34] Sanella, D. T.; Tarlecki, A., On observational equivalence and algebraic specification, J. Comput. System Sci., 34, 150-178 (1987) · Zbl 0619.68028
[35] van de Snepscheut, J. L.A., Trace Theory and VLSI Design, (Lecture Notes in Computer Science, 200 (1985), Springer: Springer Berlin) · Zbl 0616.68001
[36] Stirling, C., Modal logics for communicating systems, Theoret. Comput. Sci., 49, 311-347 (1987) · Zbl 0624.68019
[37] Widom, J.; Gries, D.; Schneider, F. B., Completeness and incompleteness of trace-baced network proof systems, Proc. 14th ACM Symp. on Principles of Progr. Languages, 27-38 (1987), München
[38] Zwiers, J., Compositionality, Concurrency and Partial correctness, (Lecture Notes in Computer Science, 321 (1989), Springer: Springer Berlin) · Zbl 0674.68011
[39] Zwiers, J.; de Roever, W. P.; van Emde-Boas, P., Compositionality and concurrent networks, (Brauer, W., Proc. 12th Coll. Automata, Languages and Programming. Proc. 12th Coll. Automata, Languages and Programming, Lecture Notes in Computer Science, 194 (1985), Springer: Springer Berlin), 509-519
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.