Abstract
As part of the Domino project on distributed system management, a model of ‘Delegation of Authority’ was created. A formal description method was used as the basis of the model in order to achieve precision and generality. Z was chosen for this purpose, supplemented by Prolog to animate the specification so that it could be validated with examples. It was found that other representation methods were necessary for visualising the model and for meaningful communication in discussions between colleagues. Three different methods were used for discussions: plain English, an ad hoc graphical method for representing domain structures and Petri net diagrams. In this paper we discuss the roles of each method of representation, its uses and limitations, and their inter-relationship. Formal interpretations in Z of the graphical methods are shown.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Castro J. and Kramer J., Temporal-Causal System Specification, Proc IEEE Conference on Computer Systems and Software, Engineering, Israel May 1990.
Dick A.J.J., Computer Aided Transformation of Prolog Specifications, Research Report 10-1702-01, 10 May 1989, Racal Research Ltd, Reading, Berks RG2 OS B.
Harel D., On Visual Formalism, Communications of the ACM, vol 31 no 5, May 1988, pp 514 - 530.
Heydon A. et al, Miro: Visual Specification of Security, IEEE Transactions on Software Engineering, vol 16 no 10, October 1990, pp 1185 - 1197.
Jensen K, High-Level Petri Nets, Advanced Course on Petri Nets, Bad Honnef Sept 1986 - GMD.
Delegation of Authority Using Domain-Based Access Rules, PhD thesis, Department of Computing, Imperial College, London, Sept 1990.
Moffett J.D. Sloman M.S. and Twidle K.P., Specifying Discretionary Access Control Policy for Distributed Systems, to appear in Computer Communications, Nov 1990.
Moffett J.D. and Sloman M.S., Delegation of Authority, Domino paper B1/IC/4, to be presented at IFIP Symposium on Integrated Network Management, Washington DC, USA, April 1991.
Delegation of Authority for Access - A Formal Model of Policy, Domino paper B 1/IC/4, submitted to 1991 IEEE Symposium on Security and Privacy.
Peterson J.L., Petri Net Theory and the Modeling of Systems, Prentice-Hall, 1981.
Stepney S. and Lord S.P., Formal Specification of an Access Control System, Software - Practice and Experience, vol 17, no 9 (Sept 1987), pp 575 - 593.
Tygar, J.D.and Wing J.M., Visual Specification of Security Constraints,IEEE Workshop on Visual Languages, Linkoping, Sweden, Aug 1987, pp 288 - 301.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Moffett, J.D., Sloman, M.S. (1991). A Case Study in Representing a Model: To Z or Not To Z?. In: Nicholls, J.E. (eds) Z User Workshop, Oxford 1990. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3540-1_16
Download citation
DOI: https://doi.org/10.1007/978-1-4471-3540-1_16
Publisher Name: Springer, London
Print ISBN: 978-3-540-19672-3
Online ISBN: 978-1-4471-3540-1
eBook Packages: Springer Book Archive