@article{LucioAmraniDingeletal.2016,
  author    = {Lucio, Levi and Amrani, Moussa and Dingel, Juergen and Lambers, Leen and Salay, Rick and Selim, Gehan M. K. and Syriani, Eugene and Wimmer, Manuel},
  title     = {Model transformation intents and their properties},
  series = {Software and systems modeling},
  volume    = {15},
  journal   = {Software and systems modeling},
  publisher = {Springer},
  address   = {Heidelberg},
  issn      = {1619-1366},
  doi       = {10.1007/s10270-014-0429-x},
  pages     = {647 -- 684},
  year      = {2016},
  abstract  = {The notion of model transformation intent is proposed to capture the purpose of a transformation. In this paper, a framework for the description of model transformation intents is defined, which includes, for instance, a description of properties a model transformation has to satisfy to qualify as a suitable realization of an intent. Several common model transformation intents are identified, and the framework is used to describe six of them in detail. A case study from the automotive industry is used to demonstrate the usefulness of the proposed framework for identifying crucial properties of model transformations with different intents and to illustrate the wide variety of model transformation intents that an industrial model-driven software development process typically encompasses.},
  language  = {en}
}
@article{JoergesMargariaSteffen2011,
  author    = {J{\"o}rges, Sven and Margaria, Tiziana and Steffen, Bernhard},
  title     = {Assuring property conformance of code generators via model checking},
  series = {Formal aspects of computing : the international journal of formal methods},
  volume    = {23},
  journal   = {Formal aspects of computing : the international journal of formal methods},
  number    = {5},
  publisher = {Springer},
  address   = {New York},
  issn      = {0934-5043},
  doi       = {10.1007/s00165-010-0169-9},
  pages     = {589 -- 606},
  year      = {2011},
  abstract  = {Automatic code generation is an essential cornerstone of today's model-driven approaches to software engineering. Thus a key requirement for the success of this technique is the reliability and correctness of code generators. This article describes how we employ standard model checking-based verification to check that code generator models developed within our code generation framework Genesys conform to (temporal) properties. Genesys is a graphical framework for the high-level construction of code generators on the basis of an extensible library of well-defined building blocks along the lines of the Extreme Model-Driven Development paradigm. We will illustrate our verification approach by examining complex constraints for code generators, which even span entire model hierarchies. We also show how this leads to a knowledge base of rules for code generators, which we constantly extend by e.g. combining constraints to bigger constraints, or by deriving common patterns from structurally similar constraints. In our experience, the development of code generators with Genesys boils down to re-instantiating patterns or slightly modifying the graphical process model, activities which are strongly supported by verification facilities presented in this article.},
  language  = {en}
}
@book{GieseBecker2013,
  author    = {Giese, Holger and Becker, Basil},
  title     = {Modeling and verifying dynamic evolving service-oriented architectures},
  publisher = {Universit{\"a}tsverlag Potsdam},
  address   = {Potsdam},
  isbn      = {978-3-86956-246-9},
  url       = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus-65112},
  publisher      = {Universit{\"a}t Potsdam},
  pages     = {97},
  year      = {2013},
  abstract  = {The service-oriented architecture supports the dynamic assembly and runtime reconfiguration of complex open IT landscapes by means of runtime binding of service contracts, launching of new components and termination of outdated ones. Furthermore, the evolution of these IT landscapes is not restricted to exchanging components with other ones using the same service contracts, as new services contracts can be added as well. However, current approaches for modeling and verification of service-oriented architectures do not support these important capabilities to their full extend.In this report we present an extension of the current OMG proposal for service modeling with UML - SoaML - which overcomes these limitations. It permits modeling services and their service contracts at different levels of abstraction, provides a formal semantics for all modeling concepts, and enables verifying critical properties. Our compositional and incremental verification approach allows for complex properties including communication parameters and time and covers besides the dynamic binding of service contracts and the replacement of components also the evolution of the systems by means of new service contracts. The modeling as well as verification capabilities of the presented approach are demonstrated by means of a supply chain example and the verification results of a first prototype are shown.},
  language  = {en}
}
@misc{Buerger2009,
  author    = {B{\"u}rger, Gerd},
  title     = {Dynamically vs. empirically downscaled medium-range precipitation forecasts},
  url       = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus-44939},
  year      = {2009},
  abstract  = {For three small, mountainous catchments in Germany two medium-range forecast systems are compared that predict precipitation for up to 5 days in advance. One system is composed of the global German weather service (DWD) model, GME, which is dynamically downscaled using the COSMO-EU regional model. The other system is an empirical (expanded) downscaling of the ECMWF model IFS. Forecasts are verified against multi-year daily observations, by applying standard skill scores to events of specified intensity. All event classes are skillfully predicted by the empirical system for up to five days lead time. For the available prediction range of one to two days it is superior to the dynamical system.},
  language  = {en}
}