Abstract
Basic architectural concepts play an important role in the design of open distributed systems. Because they are elementary notions, their clear and unambiguous understanding is essential for the understanding of the whole design. One of the key concepts of open distributed systems is the interaction point which is used to conceptually model the boundaries between the system and its environment as well as between the system's entities. Interaction points can be represented on each level of the design process and be the basis for a class of very general conformance notions.
In this paper, we investigate possible representations of the interaction point concept in the formal specification language Z. To put this investigation on a sound basis, we introduce the interaction point concept in a general way and give a list of properties which an interaction point could have. Most of these properties are formally defined. Finally, some of the Z representations are analyzed with respect to the general interaction point properties.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
6 References
Bochmann, G.v.: A General Transition Model for Protocols and Communication Services, IEEE Transactions on Communications, Vol. COM-28, No.4, April 1980, pp.643–650
Carrington, D., et, al.: Object-Z: An Object-Oriented Extension to Z, in: S. Vuong (ed.), The 2nd International Conference FORTE '89, Proc., December 5–8, 1989, Vancouver/Canada, pp.401–420
Recommendation Q.703, Specification of Signalling Link No.7, CCITT, vol. VI fascicle VI.7, Geneva, 1985
Recommendation Q.704, Specification of Signalling Link No.7, CCITT, vol. VI fascicle VI.7, Geneva, 1985
Recommendation Z.100: Specification and Description Language SDL, CCITT SG X, Contribution Com X-R 15-E, 1987
Duke, R., Hayes, I., King, P., Rose, G.: Protocol Specification and Verification Using Z, in: S. Aggarwal, K. Sabnani (eds.), Protocol Specification, Testing, and Verification VIII, North-Holland 1988, pp.33–46
Gotzhein, R.: On the Formal Definition and Representation of Architectural Concepts, Report Nr. FBI-HH-B-142/89, University of Hamburg, July 1989, 37p.
Gotzhein, R.: The Formal Definition of the Architectural Concept ‘Interaction Point', in: S. Vuong (ed.), 2nd International Conference FORTE '89, December 5–8, 1989, Vancouver, B.C., Canada, 15p.
Gotzhein, R., Heidtmann, K.: A Statement on Architectural Concepts in Conformance Testing, 2nd International Workshop on Protocol Test Systems, October 3–6, 1989, Berlin (West), F. R. Germany
Hayes, I.: Specification Case Studies, International Series in Computer Science, Prentice Hall, 1987
Hayes, I.J., Mowbray, M., Rose, G.A.: Signalling System No.7: The Network Layer, in: Protocol Specification, Testing, and Verification IX, Proc., Twente 1989, 14p.
Information Processing Systems — Open Systems Interconnection — Basic Reference Model, ISO 7498 / CCITT Recommendation X.200, October 1984
LOTOS — A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour, ISO/TC97/SC21, IS 8807, 1988
Architectural Semantics for FDTs, ISO/IEC JTC1/SC21 N3251, Dec. 1988
Guidelines for the Application of Estelle, LOTOS, and SDL, ISO/IEC JTC1/SC21/WG1 N2549 rev., Dec. 1988, 344p.
Estelle — A Formal Description Technique Based on an Extended State Transition Model, ISO/TC97/SC21, IS 9074, 1989
Koymans, R.: Specifying Message Passing Systems Requires Extending Temporal Logic, Proc. of the Sixth Annual ACM Symposium on PoDC, 1987, pp.191–204
Lichtenstein, O., Pnueli, A., Zuck, L.: The Glory of the Past, Workshop on Logics of Programs, Springer Verlag, LNCS (1985), pp.196–218
Mackert, L.F., Neumeier-Mackert, I.B.: Communicating Rule Systems, in: Proc. of the IFIP TC 6 Symposium on Protocol Specification, Testing, and Verification VII, May 5–8, 1987
Pnueli, A.: Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of Current Trends, in: Current Trends in Concurrency, LNCS 224, Springer Verlag, 1986, pp.510–584
Rescher, N., Urquhart, A.: Temporal Logic, Berlin, Springer 1971
Schwartz, R.L., Melliar-Smith, P.M.: From State Machines to Temporal Logic: Specification Methods for Protocol Standards, IEEE Transactions on Communications, No. 12, Dec. 1982, pp.2486–2496
Spivey, J.M.: The Z Notation: A Reference Manual, International Series in Computer Science, Prentice Hall, 1989
Svobodova, L.: Implementing OSI systems, IEEE Journal on Selected Areas in Communications, Vol.7, No.7, Sept. 1989, pp.1115–1130
Turner, K.: An Architectural Semantics for LOTOS, in: H. Rudin, C.H. West (eds.), Protocol Specification, Testing, and Verification, VII, North-Holland, Amsterdam, 1987
Vissers, C.A., Logrippo, L.: The Importance of the Service Concept in the Design of Data Communications Protocols, in: M. Diaz (ed.), Protocol Specification, Testing, and Verification, V, North-Holland, Amsterdam, 1986, pp.3–17
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gotzhein, R. (1990). Specifying open distributed systems with Z. In: Bjørner, D., Hoare, C.A.R., Langmaack, H. (eds) VDM '90 VDM and Z — Formal Methods in Software Development. VDM 1990. Lecture Notes in Computer Science, vol 428. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52513-0_17
Download citation
DOI: https://doi.org/10.1007/3-540-52513-0_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-52513-4
Online ISBN: 978-3-540-47006-9
eBook Packages: Springer Book Archive