Abstract
The problem of composing mutually dependent rely-guarantee specifications arises in the hierarchical development of reactive or concurrent systems. The composition principle has been proposed as a logic-independent solution to this problem. In this paper, we apply it to Unity-like rely-guarantee specifications. For that purpose, we interpret Unity formulas in Abadi and Lamport's compositional model. Then, the premises of the composition rule are reduced to proof obligations that can be carried out in the existing Unity proof system. The approach is illustrated by an example, the composition of mutually dependent specifications of concurrent buffers.
National Fund for Scientific Research (Belgium).
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
M. Abadi and L. Lamport, The Existence of Refinement Mappings, in Proceedings of the 3rd Annual Symposium on Logic In Computer Science, 1988, pp. 165–175.
M. Abadi and L. Lamport, Composing Specifications, in J.W. de Bakker, W.-P. de Roever, and G. Rozenberg eds., Stepwise Refinement of Distributed Systems, Springer-Verlag, 1990, LNCS 430, pp. 1–41.
M. Abadi and L. Lamport, An Old-Fashioned Recipe for Real Time, in J.W. de Bakker, C. Huizing, W.-P. de Roever, and G. Rozenberg eds., Real Time: Theory in Practice, Springer-Verlag, 1992, LNCS 600, pp 1–27.
M. Abadi and G.D. Plotkin, A Logical View of Composition and Refinement, in Proceedings of the 18th Annual ACM Symposium on Principles of Programming Languages, 1991, pp 323–332.
H. Bairinger, R. Kuiper, and A. Pnueli, Now you may Compose Temporal Logic Specifications, in Proceedings of the 16th ACM Symposium on Theory of Computing, 1984, pp. 51–63.
K.M. Chandy and J. Misra, Parallel Program Design: a Foundation, Addison-Wesley, 1988.
P. Collette, Semantic Rules to Compose Rely-Guarantee Specifications, Research Report RR 92-25, Université Catholique de Louvain, 1992, Belgium.
F. Dederichs, System and Environment: The Philosophers Revisited, Technical Report TUM-I 9040, Institut für Informatik, Technische Universität München, 1990, Germany.
P. Grønning, T.Q. Nielsen and H.H. Lovengreen, Refinement and Composition of Transitionbased Rely-Guarantee Specifications with Auxiliary Variables, in K.V. Nori and C.E. Veni Madhavan eds., Foundations of Software Technology and Theoretical Computer Science, Springer-Verlag, 1991, LNCS 472, pp 332–348.
C.B. Jones, Tentative Steps Towards a Development Method for Interfering Programs, in ACM Transactions on Programming Languages And Systems, 1983, Vol 5,4, pp 596–619.
B. Jonsson, On Decomposing and Refining Specifications of Distributed Systems, in J.W. de Bakker, W-P. de Roever, and G. Rozenberg eds, Stepwise Refinement of Distributed Systems, Springer-Verlag, 1990, LNCS 430, pp. 261–385.
L. Lamport, The Temporal Logic of Actions, Research Report 57, Digital Equipment Corporation Systems Research Center, 1990.
Z. Manna and A. Pnueli, The Anchored Version of the Temporal Framework, in J.W. de Bakker, W.-P. de Roever, and G. Rozenberg eds., Linear Time, Branching Time and Partial Orders in Logics and Models for Concurrency, Springer-Verlag, 1989, LNCS 354, pp. 201–284.
J. Misra and K.M. Chandy, Proofs of Networks of Processes, in IEEE Transactions on Software Engineering, 1981, Vol 7, 4, pp 417–426.
J. Misra, Specifying Concurrent Objects as Communicating Processes, in Science of Computer Programming, 1990, Vol 14, 2–3, pp. 159–184.
A. Pizzarello, An Industrial Experience in the use of UNITY, in J.P. Banâtre and D. Le Métayer eds., ResearchDirections in High-Level Parallel Programming Languages, Springer-Verlag, 1991, LNCS 574, pp 39–49.
A.K. Singh, Specification of Concurrent Objects Using Auxiliary Variables, in Science of Computer Programming, 1991, Vol 16, pp 49–88.
E.G. Stark, Proving Entailment Between Conceptual State Specifications, in Theoretical Computer Science, 1988, Vol 56, pp 135–154.
K. Stølen, A Method for the Development of Totally Correct Shared-State Parallel Programs, in J.C.M. Baeten and J.F. Groote eds., Proceedings of Concur'91, Springer-Verlag, 1991, LNCS 527, pp 510–525.
J.C.P. Woodcock and B. Dickinson, Using VDM with Rely and Guarantee-Conditions, in R. Bloomfield, L. Marshall and R. Jones eds., Proceedings of VDM'88: The Way Ahead, Springer-Verlag, 1988, LNCS 328, pp 434–458.
Q. Xu and H. Jifeng, A Theory of State-based Parallel Programming: Part I, in J. Morris ed., 4th BCS-FACS Refinement Workshop, Springer-Verlag, 1991, pp 326–359.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Collette, P. (1993). Application of the composition principle to unity-like specifications. In: Gaudel, M.C., Jouannaud, J.P. (eds) TAPSOFT'93: Theory and Practice of Software Development. CAAP 1993. Lecture Notes in Computer Science, vol 668. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56610-4_67
Download citation
DOI: https://doi.org/10.1007/3-540-56610-4_67
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56610-6
Online ISBN: 978-3-540-47598-9
eBook Packages: Springer Book Archive