Laufende Projekte

Bildung 4.0 für KMU

Wettbewerbsvorsprung im Leichtbau durch Digitales Lernen

COMBO

Kombination von Planung, Selbst-Organisation und Rekonfiguration in einem Roboterensemble zur Ausführung von ScORe-Missionen

CosiMo

Automatische Optimierung der CFK-Herstellung mit maschinellem Lernen

Flashix

Inkrementelle Verifikation nicht-lokaler Verfeinerungen für ein verifiziertes Flash-Dateisystem

KOGNIA

Teileempfehlungen für CAD-Konstruktionen mit maschinellem Lernen

Selbstorganisierende Produktion

Selbstorganisierende Produktion im Kontext von Industrie 4.0

SINA

Sichere Wahrnehmung zur flexiblen Assistenz in dynamischen und unstrukturierten Umgebungen

TeamBotS

Eine toolunterstützte Methodik zur Entwicklung von Software für dynamische Roboterteams

TeSOS

Das TeSOS-Projekt zielt darauf ab, Strategien und Techniken für das systematische (halb-)automatische Testen von selbstorganisierenden, adaptiven Systemen zu entwickeln.

WiR Augsburg

Robotergestützte Komponentenprüfung und Plug-&-Work für die Materialbearbeitung mit Industrie-4.0-Technologien

Abgeschlossene Projekte

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

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

Verifikation von nebenläufigen, lock-freien Algorithmen

OC-Trust

Koordination der DFG Forschergruppe, die sich zum Ziel gesetzt hat, soziale Konzepte (wie Vertrauen und Reputation) in selbstorganisierende Systeme zu integrieren, um deren Zuverlässigkeit als auch das Vertrauen des Nutzers in solche Systeme zu erhöhen.

ForSa@OC-Trust

In ForSa@OC-Trust werden formale Methoden, Software-Engineering-Ansätze und Algorithmen für vertrauenskritische selbstorganisierende Systeme entwickelt. Dabei steht die Gewährleistung funktionaler Korrektheit und Safety im Vordergrund.

SAVE ORCA

Eine Vorgehensweise für das systematische, top-down Entwickeln von höchst zuverlässigen selbstorganisierenden, adaptiven Systemen.

SecureMDD

A Model-Driven Development Method for Secure Applications

FORMOSA

Integrieren von Formalen Modellen und Safety Analyse

Go!Card

Formale Methoden für Secure Java Smart Cards

INOPSYS

Interoperabilität von Kalkülen zur System Modellierung

Protocure

Qualitätssicherung im Gesundheitswesen

CFK-Tex

Automated handling and placement of large dry carbon fiber textiles

Frühere Projekte

 

Vor 2000 wurden am Lehrstuhl für Softwaretechnik unter anderem folgende weiteren Projekte durchgeführt:

 

 

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.

Institut für Software & Systems Engineering

Das Institut für Software & Systems Engineering, geleitet von Prof. Dr. Wolfgang Reif, ist eine wissenschaftliche Einrichtung in der Fakultät für Angewandte Informatik an der Universität Augsburg. Das Institut unterstützt sowohl Grundlagen- als auch angewandte Forschung in allen Bereichen der Software & Systems Engineering. In der Lehre ermöglicht es die weitere Entwicklung des relevanten Kursangebots von Fakultät und Universität.

Suche