Combination of Planning, Self-Organization and Reconfiguration in a Robot Ensemble for Handling ScORe Missions
The TeSOS project aims at developing strategies and techniques for systematic (semi-)automatic testing of self-organizing, adaptive systems
A new software architecture for controlling industrial robots, combining modern software paradigms and hard real-time
Intelligent obstacle detection using capacitive sensors for safe human robot interaction
Development of an offline programming platform aimed for automizing specification of robot-based CFRP-manufacturing processes
Developing Systems with Secure Information Flow
Formal Analysis and Software Architectures for Trustworthy Self-organizing Systems @ OC-Trust
A Model-Driven Development Method for Secure Applications
Integrating FORmal MOdels and Safety Analysis
Formal Methods for Secure Java Smart Cards
Interoperability of Calculi for System Modelling
Ensuring Quality in Healthcare
Before 2000, further projects have been conducted:
DFG Research Programme "Deduction"
In a joint project on the "Integration of Automated and Interactive Theorem Proving" with the University of Karlsruhe, the KIV system was integrated with the automatic theorem provers 3TAP, Otter, Setheo and Spass.Thereby we combined the two paradigms of interactive and automatic theorem proving. We found that benefits can be drawn from using information present in KIV to control the automatic prover. The productivity of the integrated system was evaluated using the WAM case study, which proved the correctness of a compiler for Prolog to the Warren Abstract Machine (WAM).
In the SMaCOS (Secure Multiapplicative SmartCard Operating System) project a generic formal security model for multiapplicative smartcards was developed. The security model is used as a reference model in the evaluation and certification of multiapplicative smartcards according to ITSEC-criteria with the highest assurance levels E4 - E6. The formal security model is specified and verified with the VSE system. The project was a joined project with the DFKI, and was sponsored by the BSI.
Robertino Control Software
Robertino is a large industrial robot designed for use in safety critical environments like fusion reactors. In this case study we have used VSE II to construct a formal model of the distributed, concurrent control software. During our formalisation effort, we have found a safety critical error. Further details can be found in [Rock et. al. 99].
The case study was joint work with Joint Research Center (JRC) and DFKI in Saarbrücken.
In 1997, German Parliament passed the "Signaturgesetz'' which is a legal basis for the usage of digital signatures. In order to receive a certificate for critical parts of the software and organization structures related to the application of digital signatures, a formal security model has to be provided. In this case study, it has been shown that it is possible to develop such a formal security model. The process of creating and verifying digital signatures has been formally specified. The integrity and nonrepudiation of signatures has been proved. Overall 800 lines of specification were needed. See [BSI 98] for details.
The case study has been done using VSE II on behalf of the BSI. In this case study we have cooperated with the DFKI in Saarbrücken.
In the VSE project (Verification Support Environment), KIV was integrated with a case tool and the automatic theorem prover INKA. This project was sponsored by the Bundesamt für Sicherheit in der Informationstechnik (BSI). The resulting VSE system aims at correct software for critical applications, and supports for example formal specification of functional behaviour, desired design- and safety properties, modular implementation (refinement) of the functional behaviour, powerful proof support for refinement correctness, and code generation into ADA.
The VSE system is commercially available from our partners (DFKI and IST) and us. Feel free to contact us for further information.
In the BSI-project VSE-II the VSE system has been extended together with the DFKI in Saarbrücken and an industrial partner: Innovative Software Technologie (IST) in Munich. The main goals of this project have been extension of the application domain of the VSE system to distributed, reactive systems, improvements to the productivity and ergonomics of the VSE system for its use in industrial projects, development of a theorem prover which tightly integrates inductive proof strategies from the INKA theorem prover and proof strategies for programs from KIV, better deduction support for structured specifications, and transfer of development results from the KIV system to the VSE system.
Institute for Software & Systems Engineering
The Institute for Software & Systems Engineering (ISSE), directed by Prof. Dr. Wolfgang Reif, is a scientific institution within the Faculty of Applied Computer Science of the University of Augsburg. In research, the institute supports both fundamental and application-oriented research in all areas of software and systems engineering. In teaching, the institute facilitates the further development of the faculty's and university's relevant course offerings.