Abstract
We here investigate a transformation of COSY path programs which is a replacement of a single event in one path program Q by another path program P. Such a transformation, called insertion, closely corresponds to refining an atomic action into several more elementary actions. In general, the path program resulting from the insertion of P into Q has quite different behavioural properties than do P and Q. Therefore, in order to be able to use insertions as a verification tool it is necessary to develop a set of rules which would guarantee the preservation of various important properties through the insertion. One of such properties is adequacy which is a property capturing the absence of partial deadlocks in a system. In this paper we present some sufficient conditions for adequacy-preserving insertion. Also, we fully characterise the set of all those programs P for which insertion is always adequacy-preserving.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
7 References
Clarke E.M., Emerson E.A., Sistla A.P., Automatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications, TOPLAS, vol. 8(1986), pp. 244–263.
Dijkstra E.W., Finding the Correctness Proof of a Concurrent Program, Proc. Kononklijke Ned. Ak. van Wetenschappen, vol. 81(2), 1978.
Hillen D., Adequacy-preserving Substitution and Reduction Rules, Report ASM/108, Computing Laboratory, The University of Newcstle upon Tyne, 1983.
Hennessy M., Milner R., Algebraic Laws for Nondeterminism and Concurrency, JACM, vol. 32(1985), pp. 137–161.
Koutny M., A Note on Adequacy-preserving Transformations of Path Programs, Report ARM/86, Computing Laboratory, The University of Newcstle upon Tyne, 1987.
Lamport L., Proving the Correctness of Multi-Process Programs, IEEE Trans. on Soft. Eng., vol. 3(2), 1977.
Lauer P.E., The COSY Approach to Distributed Computing Systems, In: Duce D.A. (ed.), Distributed Computing Systems Programme, Peter Peregrinus, London, 1984, pp. 107–126.
Lauer P.E., Shields M.W., Cotronis J.Y., Formal Behavioural Specification of Concurrent Systems without Globality Assumptions, Lecture Notes in Computer Science, vol. 107, Springer 1981, pp. 115–151.
Murata T., Suzuki I., On the Structural Properties and Stepwise Refinment of Petri Nets, Proc. of 24th Midwest Symp. on Circuits and Systems, 1981.
Olderog E.R., Hoare C.A.R., Specification-Oriented Semantics for Communicating Processes, Acta Informatica, vol. 23(1986), pp. 9–66.
Shields M.W., Adequate Path Expressions, Lecture Notes in Computer Science, vol. 70, Springer 1979, pp. 249–265.
Shields M.W., Concurrent Machines, The Computer Journal 28,5 (1985), pp. 449–465.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1988 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Koutny, M. (1988). Adequacy-preserving transformations of COSY path programs. In: Vogt, F.H. (eds) CONCURRENCY 88. CONCURRENCY 1988. Lecture Notes in Computer Science, vol 335. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-50403-6_51
Download citation
DOI: https://doi.org/10.1007/3-540-50403-6_51
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-50403-0
Online ISBN: 978-3-540-45999-6
eBook Packages: Springer Book Archive