@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} } @misc{LamprechtNaujokatMargariaetal.2011, author = {Lamprecht, Anna-Lena and Naujokat, Stefan and Margaria, Tiziana and Steffen, Bernhard}, title = {Semantics-based composition of EMBOSS services}, series = {Postprints der Universit{\"a}t Potsdam : Mathematisch-Naturwissenschaftliche Reihe}, journal = {Postprints der Universit{\"a}t Potsdam : Mathematisch-Naturwissenschaftliche Reihe}, number = {956}, issn = {1866-8372}, doi = {10.25932/publishup-43183}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus4-431830}, pages = {23}, year = {2011}, abstract = {Background More than in other domains the heterogeneous services world in bioinformatics demands for a methodology to classify and relate resources in a both human and machine accessible manner. The Semantic Web, which is meant to address exactly this challenge, is currently one of the most ambitious projects in computer science. Collective efforts within the community have already led to a basis of standards for semantic service descriptions and meta-information. In combination with process synthesis and planning methods, such knowledge about types and services can facilitate the automatic composition of workflows for particular research questions. Results In this study we apply the synthesis methodology that is available in the Bio-jETI workflow management framework for the semantics-based composition of EMBOSS services. EMBOSS (European Molecular Biology Open Software Suite) is a collection of 350 tools (March 2010) for various sequence analysis tasks, and thus a rich source of services and types that imply comprehensive domain models for planning and synthesis approaches. We use and compare two different setups of our EMBOSS synthesis domain: 1) a manually defined domain setup where an intuitive, high-level, semantically meaningful nomenclature is applied to describe the input/output behavior of the single EMBOSS tools and their classifications, and 2) a domain setup where this information has been automatically derived from the EMBOSS Ajax Command Definition (ACD) files and the EMBRACE Data and Methods ontology (EDAM). Our experiments demonstrate that these domain models in combination with our synthesis methodology greatly simplify working with the large, heterogeneous, and hence manually intractable EMBOSS collection. However, they also show that with the information that can be derived from the (current) ACD files and EDAM ontology alone, some essential connections between services can not be recognized. Conclusions Our results show that adequate domain modeling requires to incorporate as much domain knowledge as possible, far beyond the mere technical aspects of the different types and services. Finding or defining semantically appropriate service and type descriptions is a difficult task, but the bioinformatics community appears to be on the right track towards a Life Science Semantic Web, which will eventually allow automatic service composition methods to unfold their full potential.}, language = {en} } @unpublished{KroeningMargariaWoodcock2011, author = {Kr{\"o}ning, Daniel and Margaria, Tiziana and Woodcock, Jim}, title = {Untitled}, 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-011-0201-8}, pages = {585 -- 588}, year = {2011}, language = {en} }