Abstract
This paper presents an approach for modelling interactions between users and systems in the Unifying Theories of Programming. Working in the predicate calculus, we outline generic techniques for calculating a user’s observations of a system and, in turn, for identifying the information that a user can deduce about the system’s behaviour from those observations. To demonstrate how this approach can be applied in practical software development, we propose some alternative refinement relations that offer greater flexibility than classical refinement by utilising knowledge of the observational abilities of users.
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
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall PTR, Upper Saddle River (1997)
Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall International Series in Computer Science. Prentice Hall Inc., Englewood Cliffs (1998)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL 1977: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238–252. ACM, New York (1977)
Jacob, J.L.: Refinement of shared systems. In: McDermid, J.A. (ed.) The Theory and Practice of Refinement: Approaches to the Development of Large-Scale Software Systems, pp. 27–36. Butterworths, London (1989)
Jacob, J.L.: Basic theorems about security. Journal of Computer Security 1(4), 385–411 (1992)
Denning, D.E.: Cryptography and Data Security. Addison-Wesley Longman Publishing Company, Inc., Boston (1982)
Jacob, J.L.: On the derivation of secure components. In: Proceedings of the 1989 IEEE Symposium on Security and Privacy, pp. 242–247. IEEE Computer Society, Los Alamitos (1989)
McLean, J.: A general theory of composition for trace sets closed under selective interleaving functions. In: Proceedings of the 1994 IEEE Symposium on Security and Privacy, pp. 79–93 (1994)
Mantel, H.: A Uniform Framework for the Formal Specification and Verification of Information Flow Security. PhD thesis, Universität Saarbrücken (July 2003)
Seehusen, F., Stølen, K.: Information flow security, abstraction and composition. IET Information Security 3(1), 9–33 (2009)
Roscoe, A.W., Woodcock, J.C.P., Wulf, L.: Non-interference through determinism. In: Gollmann, D. (ed.) ESORICS 1994. LNCS, vol. 875, pp. 33–53. Springer, Heidelberg (1994)
Morgan, C.: The shadow knows: Refinement and security in sequential programs. Science of Computer Programming 74(8), 629–653 (2009)
Chen, J., Hierons, R.M., Ural, H.: Conditions for resolving observability problems in distributed testing. In: de Frutos-Escrig, D., Núñez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 229–242. Springer, Heidelberg (2004)
Chen, J., Hierons, R.M., Ural, H.: Overcoming observability problems in distributed test architectures. Information Processing Letters 98(5), 177–182 (2006)
Oliveira, M., Cavalcanti, A., Woodcock, J.: A UTP semantics for Circus. Formal Aspects of Computing 21(1), 3–32 (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Banks, M.J., Jacob, J.L. (2010). On Modelling User Observations in the UTP. In: Qin, S. (eds) Unifying Theories of Programming. UTP 2010. Lecture Notes in Computer Science, vol 6445. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16690-7_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-16690-7_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16689-1
Online ISBN: 978-3-642-16690-7
eBook Packages: Computer ScienceComputer Science (R0)