A Model Transformation Semantics and Analysis Methodology for SecureUML

摘要

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.