Research direction: The main vision of our research is to design and implement practical modeling and analysis techniques for thedevelopment and maintenance of high-quality software systems. By tightly integrating flexibly transformable and incrementally verifiable models into the development process, we can manage the increasing complexity as well as heterogeneity of today's data- and software-intensive systems and the increased demands on their adaptability with a clear commitment to quality. Our approach to the design and quality assurance of software systems is therefore based on the integration of the following research areas:
- Model Engineering: for the construction of models for systems
- Transformation Engineering: for the construction of automatic (deterministic as well as search-based & randomized) methods for the transformation of systems
- Verification Engineering: for the construction of techniques (analysis, test, formal verification) that support quality assurance throughout the lifecycle of systems.
Foundations: Since the underlying structure of models can be described by graphs, graph transformation is a suitable means to specify model transformations. In addition, graph transformation also lends itself to the management and evolution of semi-structured data. We therefore use graph and graph transformation theory as solid enablers for the interplay of the above research fields. In this focus, we develop the following foundations:
- Logic and graphs: automated reasoning and SAT solving for graph properties, automated graph repair
- Graph transformation: Analysis, testing, formal verification
- Category theory for transformation systems: consolidating and unification of transformation theory for different variants of high-level structures such as typed graphs, graphs with labels, triple graphs, hypergraphs, Petri nets, attributed graphs, algebraic specifications, etc.
QA techniques: Based on these foundations, we continuously strive to develop and implement QA techniques that take into account fundamental engineering principles such as expressiveness, efficiency, usability, and generality. The overall goal is to create QA techniques that are tightly intertwined with the software development process and incorporate an appropriate degree of automation as well as human interaction. Selected examples of QA techniques we are researching include the following:
- Conflict and dependency detection in requirements specifications.
- Plausibility checking of executable models
- Verification of consistency and behavior preservation, or of the functional behavior of model transformations (especially model refactorings)
- Conformance testing of triple graph grammar implementations
- Model-based testing of graph databases and graph database applications.
Current and future example challenges and application domains focus primarily on advanced automation of design and quality assurance of data- and software-intensive systems. We intend to focus on medical informatics as one of the most important representatives in this field.