Abgeschlossene Projekte
KI-LOK － Prüfverfahren für KI-basierte Komponenten im Eisenbahnbetrieb
Im KI-LOK-Projekt wurden neue Testverfahren und wergzeuggestützte Methoden zur Absicherung und Zertifizierung von KI-gestützten Technologien für sicherheitskritische Anwendungen in der Bahntechnik erforscht.
Der Entwurf und Betrieb innovativer Fahrzeuge im schienengebundenen Verkehr fordert immer stärker den Einsatz neuartiger KI-basierter, autonomer, lernender Systeme. Das Verhalten KI-basierter Systeme ist jedoch, im Gegensatz zu bisherigen Systemen, nicht deterministisch nachvollziehbar. Dies erfordert gegenüber dem heutigen Stand der Technik adäquate, angepasste und intelligente Test- und Prüfsysteme, um die dynamischen Wechselwirkungen mit der realen Umwelt abzubilden und die Systeme auf ihre Intelligenz, Verlässlichkeit und Robustheit zu prüfen. Im Projekt wurden daher Techniken für die Validierung und Verifikation KI-basierter Systeme der Bahntechnik sowie modellbasierte Methoden zum Test von autonomen Zugsystemen erforscht. Als Fallstudien dienten dabei ein Lokführerassistenzsystem zur Objekterkennung im Lichtraumprofil des Fahrweges sowie ein visuelles Odometrie- und Positionssystem. Auf Basis dieser Ergebnisse wurden Prozesse und Werkzeugketten definiert, mit denen in Zusammenarbeit mit den nationalen und europäischen Genehmigungsbehörden eine Zulassung KI-basierter Zugsysteme zum Betrieb erreicht werden kann.
In diesem Projekt hat die HHU gezeigt, wie man mit formalen mathematischen Modellen die Sicherheit von KI-Systemen erhöhen kann und in Zukunft nachvollziehbare Sicherheitsnachweise und Zertifizierungen erreichen kann. Mit „Certifying Control“ muss die KI zusätzlich zur Ausgabe ein Zertifikat erstellen, welches von einer unabhängigen klassischen Software verifiziert werden kann. Die HHU hat gezeigt, dass für die Signalerkennung bei Rangierfahrten die „False Positive“-Rate auf fast null gesenkt werden kann. Um „False Negatives“ zu erkennen, wurde ein formales Modell zur Laufzeit benutzt, welches die KI-Ausgabe auf Plausibilität prüfen kann (und zum Beispiel fehlende Signalerkennung abfangen kann). Das formale Model ermöglicht auch die Verwendung von „Safety Shields“, welche die KI-Komponenten als Sicherheitsnetz umfasst.
Weitere Informationen finden Sie im Abschlussbericht und auf der Internetseite des Projekts.
Förderrichtlinie „Neue Fahrzeug- und Systemtechnologien“ des BMWi
Förderzeitraum: 01.04.2021 － 30.09.2024
Projektleitung HHU: Michael Leuschel
Projektpartner:
- Hitachi Rail (GTS Deutschland GmbH) － ehemals Thales Deutschland GmbH
- Fraunhofer Institut für Offene Kommunikationssysteme FOKUS
- IT Power Solutions GmbH
- neurocat GmbH
IVOIRE
Integration of Validation into a Refinement-based Rigorous Development Process
The IVOIRE project will enable continuous validation of formal models during their development by stepwise refinement. Using Event-B and Rodin, a state-of-the-art rigorous method and its support environment, IVOIRE intends to provide answers for issues associated with validation of formal specifications at three levels. At the scientific level, it proposes a formal characterization of the relation between validation and refinement. At the methodological level, it proposes an extension to the conventional notion of linear refinement that also includes validation activities called “validation obligations.” At the practical level, it proposes prototyping of new validation tools and better integration of existing ones into the specification writing process which can be used routinely to validate models.
Funded by DFG and FWF (Austria).
Partners: University of Linz, Austria.
RAPP
Responsible Academic Performance Predicton (RAPP) - Ein sozialverträglicher Ansatz zur Einführung studentischer Leistungsprognose an einer Deutschen Hochschule
Academic Performance Prediction (APP) Systeme, also Systeme zur Leistungsvorhersage, als unterstützende KI-Systeme in der Hochschulbildung versprechen die frühzeitige Erkennung von potentiellen Misserfolgen und ermöglichen damit einen gezielten Ressourceneinsatz der Hochschule um durch individuelle Unterstützungsma.nahmen diesen vorzubeugen. Allerdings wird einer an der Heinrich-Heine-Universität durchgeführten Studie zufolge der Einsatz KI-basierter Systeme von Studierenden, soweit eigene Daten und eigene Planungen betroffen sind, als problematisch betrachtet. Dies stellt ein ernsthaftes Hindernis für den Einsatz und den Erfolg solcher Systeme dar. Ziel dieses Projektes ist daher ein sozial verträglicher Einsatz von KI-Systemen, wozu ethische Aspekte und deren Wahrnehmung durch die Betroffenen erforscht werden sollen. Hierzu wird einerseits basierend auf entsprechenden Vorarbeiten ein KI-System zur Academic Performance Prediction entwickelt, in dem durch eine regelbasierte Erklärungskomponente für die Betroffenen eine weitgehende Transparenz geschaffen wird, andererseit wird der Einsatz dieses Systems, die erforderlichen Daten zur Vorhersage nach technischen und ethischen Gesichtspunkten und die Wahrnehmung durch die Studierenden durch Labor- und Feldexperimente untersucht. Hieraus sollen letztendlich Handlungsempfehlungen in Zusammenarbeit mit den verantwortlichen Stellen in der Hochschule für den Einsatz solcher Systeme abgeleitet werden.
Förderzeitraum: 01.03.2021 - 29.02.2024
BMBF (Fördermaßnahme: Digitale Hochschulbildung)
PIs: Conrad, Marcinkowski, Leuschel, Rosar
Thales Formal RBC
Thales Formal RBC war ein Forschungsprojekt mit der Firma Thales Deutschland mit dem vollständigen Projekttitel
"Software Architecture for Effective Parametric Verification and Validation of an RBC System".
Slot Tool
Ein durch die HHU gefördertes Projekt mit dem Ziel zu überprüfen, ob die Stundenpläne den juristischen Anforderungen bezüglich der Studiendauer genügen. Zum Beispiel müssen Studierende der philosophischen Fakultät in der Lage sein jede angebotene Kombination von Kern- und Ergänzungsfach im vorgesehenen Zeitrahmen (Bei Vollzeitstudium: 6 Semester) studieren zu können. Das Projekt benutzt den Constraintsolver von ProB um die Anforderungen zu überprüfen und soll es auch ermöglichen die Stundenpläne anzupassen und zu optimieren.
PyJIT
PyPy ist ein Open-Source-Projekt welches einen sehr flexible Python-Interpreter in Python selbst implementiert. Mit nur wenigen Zeilen Code ist es in PyPy möglich, zum Beispiel modernste Sicherheitsmechanismen oder alternative Nebenläufigkeitsmodelle einzubauen. Um PyPy ausgiebiger in der Praxis zu verwerten, wollen wir die Flexibilität von PyPy mit einer guten Performanz verbinden. Innerhalb des PYJIT Projektes werden wir deshalb ein "Just-In-Time"-Compiler-Toolkit entwickeln. Wir hoffen damit nicht nur flexibler sondern auch schneller als die Referenz-Implementierung von Python zu werden. Das Projekt erschließt uns damit eine große Reihe von neuen Anwendungen,zum Beispiel die Portierung von Python auf neue spezialisierte Hardware (eingebettete Systeme). Wir werden diese Techniken auch auf andere Programmiersprachen anwenden.
ProCSP
Eine Erweiterung von ProB um die Animation von CSP-M Spezifikationen, die in FDR Syntax geschrieben sind, zu ermöglichen und die Animation mit B Maschinen zu synchronisieren. Gefördert durch AWE.
Gepavas
Ein durch die DFG gefördertes Projekt das gerichtete und paralleles Model Checking von Spezifikationen auf hohem Abstraktionsniveau untersucht.
DEPLOY
Ein durch die euopäische Union im Framework 7 IP gefördertes Projekt. Das Projekt startete im Februar 2008.
Deploy Website
Advance
Ein durch die EU im Rahmen des Framework 7 STREP gefördertes Projekt. BeginL October 2011.
ADVANCE Website
ASAP
Ziel dieses Projektes ist es, Techniken zu entwickeln, die die Entwicklung von fortschrittlichen und zuverlässigen Softsystemen erlauben, die leicht zu warten sind und auf neuen Rechnerplattformen laufen können.
PyPy ist eine Re-Implementierung von Python in Python, die flexibel ist und mit der auf einfache Weise experimentiert werden kann. Unser langfristiges Ziel ist eine Portierung auf eine Vielfalt von kleinen und großen Platformen durch Bereitstellung einer Compiler Werkzeugsammlung die angepasste Python Versionen erzeugen kann. Platform, Speicher and Threading Modelle werden Aspekte des Übersetzungsprozesses anstatt Low-Level Details der Sprachimplementierung. Schlussendlich sollen auch dynamische Optimierungen als Aspekte des Übersetzungsprozesses und damit robust gegen Sprachänderungen implementiert werden.
Rodin
Ziel ist die Entwicklung einer Methodik und einer unterstützenden, erweiterbaren Tool-Platform zur kosteneffektiven, verifizierbaren Entwicklung von komplexen, zuverlässigen Software Systemen.
TSAS
Das Trusted Software Agents and Services (TSAS) project untersucht die Trust Probleme, die durch Zugriff auf Software-Systeme und Verwendung von Agenten Technologien in Computerplattformen entstehen können.
In dem Projekt werden Software und Hardeware Demos entwickelt, die zur Untersuchung von Trust im Kontext von Homebanking oder Telemedizin dienen. Das Projekt untersucht auch Validierungstechniken, die helfen können Vertrauen in derartige Techologien zu schaffen.
ABCD
Automated Validation of Business Critical Systems with Component Based Designs
Das Ziel des Projektes is die Verbreitung von formalen Methoden in geschäftskritischen Anwendungen zu verbessern. Dazu werden wir
- Die Anfangskosten senken
- Die Vorteile von formaler Modellierung verbessern
Wir werden
- Ein Repository von generischen Modellen von Systemen und Komponenten aufbauen um die Einstiegskosten zu reduzieren
- Verifikations- und Validierungstechniken Systemarchitekten zur Verfügung stellen
- Die Kosten durch automatische Werkzeuge senken
Unser Fokus liegt auf der Sefinition von Systemen und der Architektur, so dass Systemintegratoren einfach Systeme modellieren und Systemarchitekturen validieren können.
iMoc
Hauptziel des Projekts ist die Untersuchung des Potentials von automatisch abgeleiteten Abstraktionen für das Model Checking von unendlichen Zustandsräumen durch eine Kombination von bestehenden Techniken der automatischen Kontrolle von partieller Auswertung und abstrakter Interpretation.
Erste erfolgreiche Experimente wurden mit Hilfe der ECCE und LOGEN Tools durchgeführt. Das Projekt besteht aus einer theoretischen Studie zusammen mit der Implementierung eines partiellen Auswerters mit einem abstrakten Interpreter. Die Anwendbarkeit wird durch realistische Beispiele aus dem ABCD Projekt demonstriert.
IOPS
Improving Offline Program Specialization ist ein DAAD gefördertes Projekt in Kollaboration mit Germán Vidal von der Universität von Valencia.
JASP
Demonstrierbar korrekte Compilation von Java Byte Code. Dreimonatiges Projekt, das durch einen Industriepartner gefördert wurde.