Research

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.,

for the development of safety critical systems from formal requirements specifications downto executable code, including the verification of safety requirements and the correctness of implementations,
for semantical foundations of programming languages from a specification of the semantics downto a verified compiler,
for building security models and architectural models as they are needed for high level ITSEC or CC evaluations.

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.

Modelling and Analysis of Medical Guidelines

For more information see the project on ProtoCure

Object-oriented Software Engineering

Modelling with UML: Use Cases, Object Models, Communication Diagrams, Statecharts etc.
Object-oriented Development Processes: RUP, XP, Agile Development, MDA
Design Patterns
Persistence Frameworks (JDO, J2EE, hibernate, etc.)
Expertise in IDEs: JBuilder, VisualStudio, Eclipse, Together, Rational XDE
Middleware: .NET, J2EE

We teach object-oriented software engineering in

the Software Praktikum (info in German), where the students have to develop a software system proposed by an industrial partner.
the main course Software Engineering (info in German).

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 .

Security Analysis in E-Commerce Applications

Modelling of E-Commerce Applications
Security Protocols and their Analysis
Concrete Applications like: Electronic Wallets, Electronic Tickets (for railway, cinema etc.)

For more information see the project GoCard .

Specification, systematic development and verified correctness of software systems

Specification languages
Refinement of abstract designs to concrete program code
Correctness Proofs using interactive verication and model checking

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 Mechatronics & Robotics

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.

Suche

Kontakt