Research Topics

Our main areas of research are:


Interactive Theorem Proving

KIV is a tool for formal systems development. It can be employed, e.g.,

Special care was (and is) taken to provide strong proof support for all validation and verification tasks. KIV can handle large scale formal models by efficient proof techniques, multi-user support, and an ergonomical user interface. It has been used in a number of industrial pilot applications, but is also useful as an educational tool for formal methods courses. ...more

KIV projects on the WWW

A browsable representation of the formal specifications as well as the theorem bases and the proofs of some of our recent case studies, which were verified with the KIV system, can be found on our KIV projects page.

Model-based Safety Analysis

Modern computer-controlled systems are steadily increasing in complexity and at the same time failure of such systems is becoming more and more dangerous. A lot of major accidents with trains, aircrafts or power plants document this development. Therefore the need for high quality safety analysis grows, but conducting such an analysis is getting very complicated because of the systems`complexity. Model-based safety analysis aims at making safety analysis more reliable and systematic (even for complex systems).

This is achieved by combining formal models with safety techiques from engineering. Formal specifications are used to describe the system and its environment as well as for formulating safety properties. Design errors and safety flaws may then be found with verification techniques. The project investigates theoretical foundations, an integrated methodology, and provides tool support.

For more information on the results and a number of applications see the project ForMoSa.

Model-Driven Development of Secure Applications

For more information see the projects SecureMDD and IFlow.

Specification, systematic development and verified correctness of software systems

We develop the KIV system which supports the systematic development of correct software from abstract specifications to concrete code using interactive verification. Research on the combination of logic formalisms is done in the project INOPSYS. Theoretical research on refinement is focussed on the refinement of Abstract State Machines and its relation to other refinement notions like data refinement. ASM refinement has been used to verify a Prolog compiler in our project in the DFG-SPP Deduction. Refinement of Abstract Protocols specified as ASMs to Java code is also a research topic in the Go! Card project.

Organic Computing

Increasing complexity challenges traditional system design as complete specification is hardly possible with ever increasing requirements and changing tasks. Organic Computing systems approach this problem by introducing self-x properties that allow a system to react in its own way, i.e. by self-adapting to changing tasks or by self-healing if failures occur. Nevertheless this "let the system go" approach poses new challenges for designing, modeling as well as formalization and verification of such systems. Our focus is the systematic design of reliable Organic Computing applications incorporating both descriptive modeling and formal verification. For more information see the project on Organic Computing

Software-Driven Robotics & Automation

Software engineering has advanced essentially. The two major concepts are the change from imperative to object-oriented programming languages and the introduction of service-oriented architectures. During this process powerful instruments have been created to industrialize software construction. As a consequence, complex applications can be realized with a fractional amount of manpower.

The main intention of the project SoftRobot is to transfer these two concepts to industrial robotics. Therefore, a new software architecture for controlling industrial robots are being developed. The combination of modern software paradigms and the consideration of hard real-time is an innovative approach. The resulting reference architecture can change the development in industrial robotics tremendously.

Modelling and Analysis of Medical Guidelines

For more information see the project on ProtoCure

Object-oriented Software Engineering