Our main areas of research are:
- Interactive Theorem Proving
- Modelling and Analysis of Medical Guidelines
- Object-oriented Software Engineering
- Safety Analysis
- Security Analysis in E-Commerce Applications
- Specification, systematic development and verified correctness of software systems
- Systematic design of reliable organic computing applications
- Software-Driven Mechatronics & Robotics
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
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 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
- 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).
For more information on the results and a number of applications see the project ForMoSa .
- Modelling of E-Commerce Applications
- Security Protocols and their Analysis
- Concrete Applications like: Electronic Wallets, Electronic Tickets (for railway, cinema etc.)
- Specification languages
- Refinement of abstract designs to concrete program code
- Correctness Proofs using interactive verication and model checking
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.