TY - JOUR A1 - Lamprecht, Anna-Lena A1 - Margaria, Tiziana A1 - Steffen, Bernhard ED - Lambrecht, Anna-Lena ED - Margaria, Tiziana T1 - Modeling and Execution of Scientific Workflows with the jABC Framework JF - Process Design for Natural Scientists: an agile model-driven approach N2 - 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. Y1 - 2014 SN - 978-3-662-45005-5 SN - 1865-0929 IS - 500 SP - 14 EP - 29 PB - Springer Verlag CY - Berlin ER - TY - JOUR A1 - Naujokat, Stefan A1 - Neubauer, Johannes A1 - Lamprecht, Anna-Lena A1 - Steffen, Bernhard A1 - Joerges, Sven A1 - Margaria, Tiziana T1 - Simplicity-first model-based plug-in development JF - Software : practice & experience N2 - 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. KW - plug-ins KW - simplicity KW - domain-specific APIs KW - process modeling KW - bootstrapping KW - evolution KW - code generation KW - loose programming KW - dynamic service binding Y1 - 2014 U6 - https://doi.org/10.1002/spe.2243 SN - 0038-0644 SN - 1097-024X VL - 44 IS - 3 SP - 277 EP - 297 PB - Wiley-Blackwell CY - Hoboken ER - TY - GEN A1 - Ebert, Birgitta E. A1 - Lamprecht, Anna-Lena A1 - Steffen, Bernhard A1 - Blank, Lars M. T1 - Flux-P BT - automating metabolic flux analysis T2 - Postprints der Universität Potsdam : Mathematisch-Naturwissenschaftliche Reihe N2 - Quantitative knowledge of intracellular fluxes in metabolic networks is invaluable for inferring metabolic system behavior and the design principles of biological systems. However, intracellular reaction rates can not often be calculated directly but have to be estimated; for instance, via 13C-based metabolic flux analysis, a model-based interpretation of stable carbon isotope patterns in intermediates of metabolism. Existing software such as FiatFlux, OpenFLUX or 13CFLUX supports experts in this complex analysis, but requires several steps that have to be carried out manually, hence restricting the use of this software for data interpretation to a rather small number of experiments. In this paper, we present Flux-P as an approach to automate and standardize 13C-based metabolic flux analysis, using the Bio-jETI workflow framework. Exemplarily based on the FiatFlux software, it demonstrates how services can be created that carry out the different analysis steps autonomously and how these can subsequently be assembled into software workflows that perform automated, high-throughput intracellular flux analysis of high quality and reproducibility. Besides significant acceleration and standardization of the data analysis, the agile workflow-based realization supports flexible changes of the analysis workflows on the user level, making it easy to perform custom analyses. T3 - Zweitveröffentlichungen der Universität Potsdam : Mathematisch-Naturwissenschaftliche Reihe - 1054 KW - 13C metabolic flux analysis KW - MFA KW - high-throughput analysis KW - scientific workflows KW - workflow management KW - Bio-jETI Y1 - 2020 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-476696 SN - 1866-8372 IS - 1054 SP - 872 EP - 890 ER - TY - JOUR A1 - Jörges, Sven A1 - Margaria, Tiziana A1 - Steffen, Bernhard T1 - Assuring property conformance of code generators via model checking JF - Formal aspects of computing : the international journal of formal methods N2 - 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. KW - Extreme Model-Driven Development KW - Code generation KW - Model checking KW - Verification Y1 - 2011 U6 - https://doi.org/10.1007/s00165-010-0169-9 SN - 0934-5043 VL - 23 IS - 5 SP - 589 EP - 606 PB - Springer CY - New York ER - TY - JOUR A1 - Bakera, Marco A1 - Margaria, Tiziana A1 - Renner, Clemens D. A1 - Steffen, Bernhard T1 - Game-Based model checking for reliable autonomy in space JF - Journal of aerospace computing, information, and communication N2 - 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. Y1 - 2011 U6 - https://doi.org/10.2514/1.32013 SN - 1940-3151 VL - 8 IS - 4 SP - 100 EP - 114 PB - American Institute of Aeronautics and Astronautics CY - Reston ER - TY - JOUR A1 - Margaria, Tiziana A1 - Steffen, Bernhard T1 - Continuous model-driven engineering N2 - Agility at the customer, user, and application level will prove key to aligning and linking business and IT Y1 - 2009 UR - http://www.computer.org/computer/ SN - 0018-9162 ER - TY - GEN A1 - Lamprecht, Anna-Lena A1 - Margaria, Tiziana A1 - Steffen, Bernhard T1 - Bio-jETI : a framework for semantics-based service composition N2 - Background: The development of bioinformatics databases, algorithms, and tools throughout the last years has lead to a highly distributedworld of bioinformatics services. Without adequatemanagement and development support, in silico researchers are hardly able to exploit the potential of building complex, specialized analysis processes from these services. The Semantic Web aims at thoroughly equipping individual data and services with machine-processable meta-information, while workflow systems support the construction of service compositions. However, even in this combination, in silico researchers currently would have to deal manually with the service interfaces, the adequacy of the semantic annotations, type incompatibilities, and the consistency of service compositions. Results: In this paper, we demonstrate by means of two examples how Semantic Web technology together with an adequate domain modelling frees in silico researchers from dealing with interfaces, types, and inconsistencies. In Bio-jETI, bioinformatics services can be graphically combined to complex services without worrying about details of their interfaces or about type mismatches of the composition. These issues are taken care of at the semantic level by Bio-jETI’s model checking and synthesis features. Whenever possible, they automatically resolve type mismatches in the considered service setting. Otherwise, they graphically indicate impossible/incorrect service combinations. In the latter case, the workflow developermay either modify his service composition using semantically similar services, or ask for help in developing the missing mediator that correctly bridges the detected type gap. Newly developed mediators should then be adequately annotated semantically, and added to the service library for later reuse in similar situations. Conclusion: We show the power of semantic annotations in an adequately modelled and semantically enabled domain setting. Using model checking and synthesis methods, users may orchestrate complex processes from a wealth of heterogeneous services without worrying about interfaces and (type) consistency. The success of this method strongly depends on a careful semantic annotation of the provided services and on its consequent exploitation for analysis, validation, and synthesis. We are convinced that these annotations will become standard, as they will become preconditions for the success and widespread use of (preferred) services in the Semantic Web T3 - Zweitveröffentlichungen der Universität Potsdam : Mathematisch-Naturwissenschaftliche Reihe - paper 136 KW - European Bioinformatics Institute KW - Integration KW - Tool KW - Alignment KW - Workflow Y1 - 2009 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-45066 ER - TY - BOOK A1 - Margaria, Tiziana A1 - Kubczak, Christian A1 - Steffen, Bernhard T1 - Bio-jETI: a Service Integration, Design, and Provisioning Platform for Orchestrated Bioinformatics Processes - ("part of From Components to Processes") T3 - Preprint / Universität Potsdam, Institut für Informatik Y1 - 2007 SN - 0946-7580 VL - 2007, 4 PB - Univ. CY - Potsdam ER - TY - BOOK A1 - Lamprecht, Anna-Lena A1 - Magaria, Tiziana A1 - Steffen, Bernhard A1 - Sczyrba, Alexander A1 - Hartmeier, Sven A1 - Giegerich, Robert T1 - GeneFisher-P BT - Variations of GneFisher as Process in Bio jETI - (part of "From Components to Processes") T3 - Preprint / Universität Potsdam, Institut für Informatik Y1 - 2007 SN - 0946-7580 VL - 2007, 3 PB - Univ. CY - Potsdam ER -