Schwerpunkte

Today’s development of modern software-based systems is characterized by

• vaguely defined problems as the result of some requirements engineering,
• typically expressed in natural language or, in the best case, in a semi-formal notation,
• implemented on top of large software libraries or other third party code as an overall system of millions of lines of code to
• run on a highly complex enterprise environment, which may even critically involve services connected via wide area networks, i.e., the Internet, and it should, of course, be
• easily adaptable to changing requests.

Practice answers these requests with quite some success with approaches like extreme programming and Scrum, which essentially replace any kind of foundational method by close cooperation and communication within the team and with the customer, combined with early prototyping and testing. It seems that this state-of-the-art reduces the role of the classical formal methods-based approaches in the sense of Hoare and Dijkstra to the niche of (extremely) safety-critical systems, simply because two things are unclear:

• What should be formally verified in cases where the problem is not stated precisely upfront? In fact, in most software projects, adapting the development to the changing needs revealed last-minute is the dominating task.
• What does a fully verified program help, if it comes too late? In fact, in many projects the half-life period is far too short to accomodate any verification activities.

Our research focuses on methods and tools to optimally live in a world where change is no exception, but the norm. We select, adapt, and enhance known (formal) methods to complement the state-of-the-art of today’s agile programming in a fashion that supports cooperative development and controlled division of labor to a point where application experts are empowered to overtake the bulk of required day-to-day changes themselves. Conceptually, our work which is designed to exploit domain-specificity, bases on three lines of research and development:

• Metamodeling for domain specialization comprises the definition of adequate metamodels and ontologies for generating domain-specific graphical tools that support controlled user-level modeling and semantics-preserving model transformations. Tools generated with the Cinco Framework allow application experts to work in a dedicated graphical environment tailored to their specific needs without being bothered by tedious syntax or complex system constraints. DyWA takes user-level domain modeling to the web in a prototype-driven and agile fashion. Its focus lies in supporting to change the application domain frequently in a running system without juggling with technical details.
• User-level constraint-guided graphical process modelling includes process simulation, model checking, code generation, and runtime verification via automated testing. The process modelling framework jABC is unique in supporting key modelling features like easy integration of new functional blocks (business activities)(cite), explicite typing and higher-order process modelling, as well as full code generation with the Genesys framework in combination with automated deployment even for specialized hardware or system environments, which make it an ideal framework for dealing with variability and software product lines at the user-level.
• Behaviour-based runtime validation is a technology based on active automata learning. Due to its high degree of automation, this technology is particularly suited for continuous validation during agile development. In fact, its underlying test-based model construction does not only steer the testing process. Rather, the inferred models are ideal means to follow the systems’ evolution via visual inspection of highlighted differences between the models of subsequent versions.

We are convinced that these three lines of research and development in combination will have a major impact on future systems’ development, in particular when it comes to mastering change.