@Article{	  brucker.ea:mda:2007,
  abstract	= {We present a model-driven architecture (MDA) framework
		  that integrates formal analysis techniques into an
		  industrial software development process model. This
		  comprises modeling using UML/OCL, processing models by
		  model transformations, code generation (including
		  runtime-test environments) and formal analysis using the
		  theorem proving environment HOL-OCL. Moreover, our
		  frameworks supports the verification of proof obligations
		  that are generated during model transformations.We show the
		  extensibility of our approach by providing a SecureUML
		  extension of the framework, which allows for an integrated
		  specification of security properties, their analysis and
		  their conversion to code.},
  author	= {Achim D. Brucker and J\"urgen Doser and Burkhart Wolff},
  journal	= {Electronic Communications of the EASST},
  language	= {USenglish},
  pdf		= {papers/2007/easst-framework.pdf},
  title		= {An {MDA} Framework Supporting {OCL}},
  volume	= 5,
  year		= 2007,
  user		= {doserj}
}