A Model Transformation Semantics and Analysis Methodology for SecureUML

By Achim D. Brucker, Jürgen Doser, and Burkhart Wolff.

SecureUML is a security modeling language for formalizing access control requirements in a declarative way. It is equipped with a UML notation in terms of a UML profile, and can be combined with arbitrary design modeling languages. We present a semantics for SecureUML in terms of a model transformation to standard UML/OCL. The transformation scheme is used as part of an implementation of a tool chain ranging from front-end visual modeling tools over code-generators to the interactive theorem proving environment HOL-OCL. The methodological consequences for an analysis of the generated OCL formulae are discussed.

Keywords:
Security, SecureUML, UML, OCL, HOL-OCL, Model-Transformation

Supplementary material:
[ Slides  ]

Extended by:
An extended version is available as:
A. D. Brucker, J. Doser, and B. Wolff, “A model transformation semantics and analysis methodology for SecureUML,” ETH Zurich, 524, 2006. Author copy: https://logicalhacking.com/publications/brucker.ea-transformation-2006-b/

Please cite this work as follows:
A. D. Brucker, J. Doser, and B. Wolff, “A model transformation semantics and analysis methodology for SecureUML,” in MoDELS 2006: Model driven engineering languages and systems, O. Nierstrasz, J. Whittle, D. Harel, and G. Reggio, Eds. Heidelberg: Springer-Verlag, 2006, pp. 306–320. doi: 10.1007/11880240_22. An extended version of this paper is available as ETH Technical Report, no. 524.

BibTeX
@InCollection{ brucker.ea:transformation:2006,
  abstract   = {SecureUML is a security modeling language for formalizing
                access control requirements in a declarative way. It is
                equipped with a UML notation in terms of a UML profile, and
                can be combined with arbitrary design modeling languages. We
                present a semantics for SecureUML in terms of a model
                transformation to standard UML/OCL. The transformation scheme
                is used as part of an implementation of a tool chain ranging
                from front-end visual modeling tools over code-generators to
                the interactive theorem proving environment HOL-OCL. The
                methodological consequences for an analysis of the generated
                OCL formulae are discussed.},
  keywords   = {Security, SecureUML, UML, OCL, HOL-OCL,
                Model-Transformation},
  location   = {Genova},
  author     = {Achim D. Brucker and J\"urgen Doser and Burkhart Wolff},
  booktitle  = {{MoDELS} 2006: Model Driven Engineering Languages and
                Systems},
  language   = {USenglish},
  publisher  = {Springer-Verlag },
  address    = {Heidelberg },
  series     = {Lecture Notes in Computer Science },
  doi        = {10.1007/11880240_22},
  number     = {4199},
  pages      = {306--320},
  editor     = {Oscar Nierstrasz and Jon Whittle and David Harel and Gianna
                Reggio},
  title      = {A Model Transformation Semantics and Analysis Methodology for
                {SecureUML}},
  areas      = {security, formal methods, software},
  extendedby = {brucker.ea:transformation:2006-b},
  year       = {2006},
  note       = {An extended version of this paper is available as ETH
                Technical Report, no. 524.},
}