Current projects

COMBO

Combination of Planning, Self-Organization and Reconfiguration in a Robot Ensemble for Handling ScORe Missions

KoARob

Kombination von unterschiedlichen nicht-sicheren Sensorsystemen zu einem funktional sicheren Gesamtsystem für den Einsatz in der Mensch-Roboter-Kollaboration

Self-organizing Production

Self-organizing Production in the context of Industry 4.0

TeamBotS

A tool-based methodology for developing software for dynamic robot teams

VeriCode

Correct Translation of Abstract Specifications to C-Code

WiR Augsburg

Robotic component inspection and Plug-&-Work for composite materials processing in concert with Industry 4.0 technologies

FORinFPRO

Intelligent manufacturing processes & Closed-loop production

Completed Projects

AICUT

Automated detection of process disturbances and quality deviations in machining production with machine learning

Flashix

Construction and Verification of a State-of-the-Art File System for Flash Memory

KOGNIA

Machine Learning based Part Recommendations for CAD Constructions

TeSOS

The TeSOS project aims at developing strategies and techniques for systematic (semi-)automatic testing of self-organizing, adaptive systems

Bildung 4.0 für KMU

Digital learning as a competitive advantage in light-weight production

CosiMo

Automatic Optimization of CFRP Production with Machine Learning

SoftRobot

A new software architecture for controlling industrial robots, combining modern software paradigms and hard real-time

SafeAssistance

Intelligent obstacle detection using capacitive sensors for safe human robot interaction

SINA

Reliable Perception for Flexible Assistance in Dynamic and Unstructured Environments

CFK-OPP

Development of an offline programming platform aimed for automizing specification of robot-based CFRP-manufacturing processes

IFlow

Developing Systems with Secure Information Flow

VeriCAS

Verification of Fine-Grained Concurrent Algorithms

OC-Trust

Coordination of the DFG Research Group on Trustworthyness in Self-organizing Systems

ForSa@OC-Trust

Formal Analysis and Software Architectures for Trustworthy Self-organizing Systems @ OC-Trust

SAVE ORCA

Systematic design of reliable Organic Computing applications

SecureMDD

A Model-Driven Development Method for Secure Applications

FORMOSA

Integrating FORmal MOdels and Safety Analysis

Go!Card

Formal Methods for Secure Java Smart Cards

INOPSYS

Interoperability of Calculi for System Modelling

Protocure

Ensuring Quality in Healthcare

CFK-Tex

Automated handling and placement of large dry carbon fiber textiles

Previous Projects

 

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

SMaCOS

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.

Digital Signatures

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.

VSE

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.

VSE II

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.

Search