Abstract
We unify the parallel composition rule of assumption-commitment specifications for respectively state-based and message-based concurrent processes. Without providing language-dependent definitions, we first assume that the model of a process can be given as a set of ‘sequences’ (e.g., traces, state sequences). Then we assume the existence of a merging operator that captures the compositionality of that model. On this basis, we formulate a semantic parallel composition rule for assumptioncommitment specifications wherein the merging operator behaves as a parameter. Then, by providing suitable language-specific definitions for the model of a process and the merging operator, we transform the semantic rule into syntactic ones, both for the state-based and message-based approaches to concurrency.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Abadi, M., Lamport, L.: An old-fashioned recipe for real time. In: de Bakker, J.W., Huizing, C., de Roever, W.-P., Rozenberg, G. (eds.) Real time: theory in practice. (Lect. Notes Comput. Sci., vol. 600, pp 1–27) Springer-Verlag 1992
Abadi, M., Lamport, L.: Composing specifications. ACM Trans. on Prog. Lang. and Syst. 15 (1), 73–132 (1993)
Abadi, M., Lamport, L.: Conjoining specifications, Digital Equipment Corporation Systems Research Center, Research Report 118, 1993.
Abadi, M., Plotkin, G.D.: A logical view of composition. TCS 114 3–30 (1993)
Aczel, P.: On an inference rule for parallel composition. Unpublished, University of Manchester 1983
Barringer, H., Kuiper, R., Pnueli, A.: Now you may compose temporal logic specifications. In: Proc. 16th ACM Symposium on Theory of Computing, pp. 51–63 1984
Barringer, H., Kuiper, R., Pnueli, A.: A compositional temporal approach to a CSP-like language. In: Neuhold, E.J., Chroust, G. (eds.) Formal Models of Programming. Elsevier 1985
Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. ACM 31, 560–599 (1984)
Broy, M.: Functional specification of time-sensitive communicating systems. ACM Trans. on Soft. Eng. and Meth. 2 (1), 1–46 (1993)
Cau, A., Kuiper, R., de Roever, W.-P.: Formalizing Dijkstra’s development strategy within Stark’s formalism. In: Jones, C.B., Shaw, R.C. Denvir, T. (eds.) Proc. 5th BCS-FACS Refinement Workshop, pp 4–42. Springer-Verlag 1992
Collette, P.: Application of the composition principle to UNITY-like specifications. In: Gaudel, M.-C., Jouannaud, J.-P., (eds.) Proc. TAPSOFT ’93. (Lect. Notes Comput. Sci., vol 668, pp 230–242) Springer-Verlag 1993
Collette, P.: An explanatory presentation of composition rules for assumption-commitment specifications. Inf. Proc. Letters 50, 31–35 (1994)
Collette, P.: Design of compositional proof systems based on assumption-commitment specifications —Application to UNITY. Ph.D. Thesis, Université Catholique de Louvain, 1994.
Grønning, P., Nielsen, T.Q., Lovengreen, H.H.: Refinement and composition of transition-based relyguarantee specifications with auxiliary variables. In: Veni Madhavan, C.E., Nori, K.V. (eds.) Proc. Foundations of Software Technology and Theoretical Computer Science. (Lect. Notes Comput. Sci., vol 472, pp 332–348) Springer-Verlag 1991
Hennessy, M: The semantics of programming languages. Wiley 1990
Jones, C.B.: Development methods for computer programs including a notion of interference. Ph.D. Thesis, Oxford University, 1981.
Jones, C.B.: Tentative steps towards a development method for interfering programs. ACM Trans. on Prog. Lang. and Syst. 5 (4), 596–619 (1983)
Misra, J., Chandy, K.M.: Proofs of networks of processes. IEEE Trans. on Soft. Eng., 7 (4), 417–426 (1981)
Pandya, P.K.: Compositional verification of distributed programs. Ph.D. Thesis, University of Bombay 1988.
Pandya, P.K.: Some comments on the assumption-commitment framework for compositional verification of distributed programs. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) Stepwise refinement of distributed systems. (Lect. Notes Comput. Sci., vol 430, pp 622–640) Springer-Verlag 1990
Pandya, P.K., Joseph, M.: P-A logic —a compositional proof system for distributed programs. Distrib. Comp. 5, 37–54 (1991)
Pnueli, A: In transition from global to modular temporal reasoning about programs. In: Apt, K.R. (ed.) Logics and models of concurrent systems. (NATO ASI Series, vol F 13, pp 123–144) Springer-Verlag 1985
de Roever, W.-P.: The quest for compositionality —a survey of assertion based proof systems for concurrent programs, Part I. In Proc. of IFIP Working Conference: The Role of Abstract Models in Computer Science, North-Holland, 1985.
de Roever, W.-P., Hooman, J., de Boer, F., Lakhneche, Y., Xu, Q., Pandya, P.: State-based proof theory of concurrency: from noncompositional to compositional methods. Book manuscript, 350 pages, Christian-Albrechts-Universität zu Kiel, Germany, 1994
Stark, E.W.: A proof technique for rely/guarantee properties. In: Proc. Foundations of Software Technology and Theoretical Computer Science. (Lect. Notes Comput. Sci., vol 206, pp 369–391) Springer-Verlag 1985
Stirling, C.: A generalization of Owicki-Gries Hoare logic for a concurrent while language. TCS 58, 347–359 (1988)
Stølen, K.: A method for the development of totally correct shared-state parallel programs. In: Baeten, J.C.M., Groote, J.F., (eds.), Proc. Concur ’91. (Lect. Notes Comput. Sci., vol 527, pp 510–525.) Springer-Verlag 1991
Stølen, K., Dederichs, F., Weber, R.: Assumption/commitment rules for networks of asynchronously communicating agents. Technical Report SFB 342/2/93, Technical University of Munich 1993
Woodcock, J.C.P., Dickinson, B.: Using VDM with rely and guarantee-conditions, in Bloomfield, R., Marshall, L., Jones, R. (eds.). Proc. VDM ’88, The Way Ahead. (Lect. Notes Comput. Sci., vol 328, pp 434–458.) Springer-Verlag 1988
Xu, Q., He, J.: A theory of state-based parallel programming: Part I. In Morris, J. (ed.) Proc. 4th BCS-FACS Refinement Workshop, pp 326–359. Springer-Verlag 1991
Zwiers, J., de Bruin, A., de Roever, W.-P.: A proof system for partial correctness of dynamic networks of processes. In: Proc. Conference on Logics of Programs 1983. (Lect. Notes Comput. Sci., vol 164, pp 513–527) Springer-Verlag 1984
Zwiers, J., de Roever, W.-P., van Emde Boas,P.: Compositionality and concurrent networks: soundness and completeness of a proof system. Technical Report 57, University of Nijmegen 1984.
Zwiers, J.: Compositionality, concurrency and partial correctness. (Lect. Notes Comput. Sci., vol 321) Springer-Verlag 1989
Author information
Authors and Affiliations
Additional information
Partially Supported by ESPRIT Project 6021 (REACT).
Supported by National Fund for Scientific Research (Belgium)
Rights and permissions
About this article
Cite this article
Cau, A., Collette, P. Parallel composition of assumption-commitment specifications. Acta Informatica 33, 153–176 (1996). https://doi.org/10.1007/s002360050039
Received:
Issue Date:
DOI: https://doi.org/10.1007/s002360050039