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

Please cite this work as follows:
A. D. Brucker, J. Doser, and B. Wolff, “A model transformation semantics and analysis methodology for SecureUML,” ETH Zurich, 524, 2006. Author copy: http://logicalhacking.com/publications/brucker.ea-transformation-2006-b/

BibTeX
@TechReport{ brucker.ea:transformation:2006-b,
  author      = {Achim D. Brucker and J{\"u}rgen Doser and Burkhart Wolff},
  institution = {ETH Zurich},
  language    = {USenglish},
  title       = {A Model Transformation Semantics and Analysis Methodology for
                 {SecureUML}},
  areas       = {security, formal methods, software},
  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},
  year        = {2006},
  number      = {524},
  num_pages   = {18},
  note        = {Author copy: \url{http://logicalhacking.com/publications/brucker.ea-transformation-2006-b/}},
}