Integrating conventional and formal methods of software engineering

The need to employ formally based methods in software development, e.g., with safety critical software, is being increasingly honoured as an alternative to (conventional) software engineering since it enables, e.g., early simulation, verification and automatic test case generation. On the other hand, insights and procedures of (conventional) software engineering have stood the test in practice. Therefore, it is our goal to combine the advantages of both approaches, viz. conventional "best practices" and formal methods of software engineering, to obtain an integrated software development methodology in terms of a generally accepted science of construction. This comprises not only theoretical and methodological aspects but also tools and applications.


ENsurance of Software evolUtion by Run-time cErtification

Model Driven Development

Many available software modelling tools are little helpful for developers, since they are often used only for documentation purposes or they can only generate code scaffolds from static models. The consequence is that models from the analysis and design phases are not sufficiently maintained during the implementation and thus no longer reflect the current state of code. We investigate the construction of more powerful software tools that are able to support and/or guarantee the synchronisation of analysis/design and implementation artefacts without limiting the developer in his present implementation capabilities.
Some relevant topics are:

  • MDD (Model Driven Development): code generation and meta-modelling
  • MDA (Model Driven Architecture)
  • Using UML 2.0 to model and simulate behaviour
  • Compiler construction
  • Enterprise Design Patterns


Interpreter und Debugger für UML 2 Aktivitätsdiagramme

Constraint Handling Rules (CHR)

Constraint Handling Rules (CHR) is a concurrent committed-choice constraint logic programming language consisting of guarded rules that transform multi-sets of atomic formulas (constraints) until exhaustion. It was designed by Thom Frühwirth in 1991.

CHR can embed many rule-based formalisms and systems, and it can describe algorithms in a compact declarative way without compromising efficiency. The clean semantics of CHR ensures that several desirable properties hold for CHR programs and also facilitates sophisticated program analysis. Dozens of CHR libraries exist for programming languages such as Prolog, Java and Haskell.

So far, worldwide more than 200 academic and industrial projects use CHR and 2000 research publications investigate CHR. There is a yearly workshop and a biannual summer school on CHR.

Constraint Programming and Reasoning

The use of constraints had its scientific and commercial breakthrough in the 1990s. Programming with constraints makes it possible to model and specify problems with uncertain, incomplete information and to solve combinatorial problems, as they are abundant in industry and commerce, such as scheduling, planning, transportation, resource allocation, layout, design, and analysis.

Constraint-based programming languages enjoy elegant theoretical properties, conceptual simplicity, and practical success. The idea of constraint-based programming is to solve problems by simply stating constraints (conditions, properties) which must be satisfied by a solution of the problem. Constraints can be considered as pieces of partial information. Constraints describe properties of unknown objects and relationships between them. Constraints are formalized as distinguished, predefined predicates in first-order predicate logic. The unknown objects are modeled as variables.

This project investigates various aspects of constraint programming.


Automatic Support for Proving Confluence Modulo Equivalence for CHR

Experimental software engineering

To improve the quality of software development in a systematic and traceable way one needs a description of the quality aims that can be measured. It is only with such a quantitative basis that one can objectively determine quality characteristics in process and project development to use them in planning, supervising, and controlling software development. Within this scope we experimentally investigate current topics in the field of embedded systems (usually in co-operation with DaimlerChrysler Research Ulm). In particular we aim at obtaining reliable data on systematic development and analytic quality assurance.

Program transformation / Ultra

Program transformation characterises a methodology of software development where one derives a program from a formal, usually functional or declarative specification by stepwise application of semantics-preserving transformation rules. The resulting program is not only correct by construction, i.e., fulfils its specification, but may also meet further important criteria such as efficiency.
A concrete result of the application of this approach to functional programming is the interactive, prototypic transformation system Ultra, which offers a good basis for further studies in the context of formal program development.


Visualisierung von Haskell Programmen als Datenfluss Diagramme

Requirements engineering

Requirements engineering deals with methods, formalisms and tools to identify, formulate and analyse requirements for software-based systems. The primary idea of our activities in requirements engineering is the creation of models. A model is an abstract, largely formal description of a system that allows to specify requirements without anticipating the implementation, while it enables the analysis of a system's structure and behaviour as soon as possible during its development.
Concrete topics are:

  • foundations, connections, interfaces, and the integration of different existing approaches
  • coexistence and the blending of different formalisms
  • criteria for consistency and completeness of models or precise semantic definitions of particular modelling concepts
  • methodology and computer support for the development of (formal) specifications from informal problem statements
  • application of formal methods
  • general aspects of tool support for requirements engineering