@article{MargariaSteffen2009,
  author    = {Margaria, Tiziana and Steffen, Bernhard},
  title     = {Continuous model-driven engineering},
  issn      = {0018-9162},
  year      = {2009},
  abstract  = {Agility at the customer, user, and application level will prove key to aligning and linking business and IT},
  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}
}
@article{BakeraMargariaRenneretal.2011,
  author    = {Bakera, Marco and Margaria, Tiziana and Renner, Clemens D. and Steffen, Bernhard},
  title     = {Game-Based model checking for reliable autonomy in space},
  series = {Journal of aerospace computing, information, and communication},
  volume    = {8},
  journal   = {Journal of aerospace computing, information, and communication},
  number    = {4},
  publisher = {American Institute of Aeronautics and Astronautics},
  address   = {Reston},
  issn      = {1940-3151},
  doi       = {10.2514/1.32013},
  pages     = {100 -- 114},
  year      = {2011},
  abstract  = {Autonomy is an emerging paradigm for the design and implementation of managed services and systems. Self-managed aspects frequently concern the communication of systems with their environment. Self-management subsystems are critical, they should thus be designed and implemented as high-assurance components. Here, we propose to use GEAR, a game-based model checker for the full modal mu-calculus, and derived, more user-oriented logics, as a user friendly tool that can offer automatic proofs of critical properties of such systems. Designers and engineers can interactively investigate automatically generated winning strategies resulting from the games, this way exploring the connection between the property, the system, and the proof. The benefits of the approach are illustrated on a case study that concerns the ExoMars Rover.},
  language  = {en}
}
@article{LamprechtMargariaSteffen2014,
  author    = {Lamprecht, Anna-Lena and Margaria, Tiziana and Steffen, Bernhard},
  title     = {Modeling and Execution of Scientific Workflows with the jABC Framework},
  series = {Process Design for Natural Scientists: an agile model-driven approach},
  journal   = {Process Design for Natural Scientists: an agile model-driven approach},
  number    = {500},
  editor    = {Lambrecht, Anna-Lena and Margaria, Tiziana},
  publisher = {Springer Verlag},
  address   = {Berlin},
  isbn      = {978-3-662-45005-5},
  issn      = {1865-0929},
  pages     = {14 -- 29},
  year      = {2014},
  abstract  = {We summarize here the main characteristics and features of the jABC framework, used in the case studies as a graphical tool for modeling scientific processes and workflows. As a comprehensive environment for service-oriented modeling and design according to the XMDD (eXtreme Model-Driven Design) paradigm, the jABC offers much more than the pure modeling capability. Associated technologies and plugins provide in fact means for a rich variety of supporting functionality, such as remote service integration, taxonomical service classification, model execution, model verification, model synthesis, and model compilation. We describe here in short both the essential jABC features and the service integration philosophy followed in the environment. In our work over the last years we have seen that this kind of service definition and provisioning platform has the potential to become a core technology in interdisciplinary service orchestration and technology transfer: Domain experts, like scientists not specially trained in computer science, directly define complex service orchestrations as process models and use efficient and complex domain-specific tools in a simple and intuitive way.},
  language  = {en}
}
@article{NaujokatNeubauerLamprechtetal.2014,
  author    = {Naujokat, Stefan and Neubauer, Johannes and Lamprecht, Anna-Lena and Steffen, Bernhard and Joerges, Sven and Margaria, Tiziana},
  title     = {Simplicity-first model-based plug-in development},
  series = {Software : practice \& experience},
  volume    = {44},
  journal   = {Software : practice \& experience},
  number    = {3},
  publisher = {Wiley-Blackwell},
  address   = {Hoboken},
  issn      = {0038-0644},
  doi       = {10.1002/spe.2243},
  pages     = {277 -- 297},
  year      = {2014},
  abstract  = {In this article, we present our experience with over a decade of strict simplicity orientation in the development and evolution of plug-ins. The point of our approach is to enable our graphical modeling framework jABC to capture plug-in development in a domain-specific setting. The typically quite tedious and technical plug-in development is shifted this way from a programming task to the modeling level, where it can be mastered also by application experts without programming expertise. We show how the classical plug-in development profits from a systematic domain-specific API design and how the level of abstraction achieved this way can be further enhanced by defining adequate building blocks for high-level plug-in modeling. As the resulting plug-in models can be compiled and deployed automatically, our approach decomposes plug-in development into three phases where only the realization phase requires plug-in-specific effort. By using our modeling framework jABC, this effort boils down to graphical, tool-supported process modeling. Furthermore, we support the automatic completion of process sketches for executability. All this will be illustrated along the most recent plug-in-based evolution of the jABC framework, which witnessed quite some bootstrapping effects.},
  language  = {en}
}