新万博体育下载_万博体育app【投注官网】

图片

Laufende Projekte

COMBO

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

KoARob

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

Selbstorganisierende Produktion

Selbstorganisierende Produktion im Kontext von Industrie 4.0

TeamBotS

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

VeriCode

Korrekte ?bersetzung abstrakter Spezifikationen in C-Programme

WiR Augsburg

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

FORinFPRO

Intelligente Fertigungsprozesse & Closed-Loop-Produktion

Abgeschlossene Projekte

AICUT

Maschinelles Lernen zur Qualit?tsvorhersage und Reduktion von Postprozess-Messungen in der Zerspanung

Flashix

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

KOGNIA

Konstruktionsunterstützung in CAD mit maschinellem Lernen und künstlicher Intelligenz

TeSOS

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

Bildung 4.0 für KMU

Wettbewerbsvorsprung im Leichtbau durch Digitales Lernen

CosiMo

Automatische Optimierung der CFK-Herstellung mit maschinellem Lernen

SINA

Sichere Wahrnehmung zur flexiblen Assistenz in dynamischen und unstrukturierten Umgebungen

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 新万博体育下载_万博体育app【投注官网】 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