Förderprojekte

Förderbeginn 01.07.2010

Satisfiability Modulo Theories für Diagnose und Steuerung Hybrider Systeme

Dr. Martin Sachenbacher
Technische Universität München
Lehrstuhl für Informatik

Dr. Natarajan Shankar
SRI International
Computer Science Laboratory

Zunehmende Rechenleistung in eingebetteten Systemen ermöglicht intelligente technische Systeme, die basierend auf einem Modell des Systems und seiner Umgebung laufend den aktuellen Systemzustand einschätzen und kostenoptimale Aktionen planen, um gewünschte Zustände zu erreichen bzw. Fehler automatisch zu beheben. Anwendungen umfassen flexible Produktionsysteme, die sich für die Herstellung individueller Produkte konfigurieren und optimieren, oder interaktive Stromnetze, deren Komponenten selbsttätig entscheiden, Strom zu laden oder zurückzuspeisen. Ziel dieses Projekts ist, gemeinsam eine effiziente Softwarekomponente für die modellbasierte Überwachung, Diagnose und Steuerung von technischen Systemen zu entwickeln. Diese wird auf gewichteten Satisfiability Modulo Theories (SMT) als zugrundeliegende Modellierungssprache aufsetzen, um sowohl diskrete als auch kontinuierliche Dynamiken wie beispielsweise Transportprozesse oder Lade/Entladevorgänge kompakt abzubilden. Der entstehende Prototyp soll in der kognitiven Fabrik der TUM und einem Vehicle-to-Grid-Prüfstand evaluiert werden.

Abschlussbericht
Das Projekt zielte auf neuartige Modellierungstechniken und Algorithmen für gemischt diskret-kontinuierliche (hybride) Systeme, welche logik-basierte Repräsentationen mit reellwertiger Arithmetik kombinieren. Dazu haben wir insbesondere den beim Kooperationspartner SRI entwickelten SMT-Solver Yices untersucht und experimentell eingesetzt, um zu beurteilen inwiefern sich dieser Ansatz für die automatische Erkennung und Kontrolle von Fehlern in hybriden technischen Systemen wie Smart Factories oder Energiesystemen eignet. Die Anschubfinanzierung ermöglichte einen einmonatigen Forschungsaufenthalt von Paul Maier bei SRI im Jahr 2010 und einen Besuch von Martin Sachenbacher bei SRI im Jahr 2011, bei denen Ideen und Konzepte diskutiert und zum Teil auch experimentell validiert werden konnten. Umgekehrt hielt SRI-Mitarbeiter Wilfried Steiner im Jahr 2011 einen eingeladenen Vortrag in München. Ergebnisse der Zusammenarbeit wurden in einem technischen Bericht und zwei Publikationen [1,2] dokumentiert. Unsere laufende Forschung zielt auf die Ausweitung des Ansatzes zur Analyse der funktionalen Sicherheit in hybriden Systemen [3].

Referenzen

[1] Paul Maier, Dominik Jain, and M. Sachenbacher: Compiling AI Engineering Models for Probabilistic Inference. German Conference on Artificial Intelligence (KI), Berlin, Germany, 2011.

[2] Paul Maier, Dominik Jain and Martin Sachenbacher: Diagnostic Hypothesis Enumeration vs. Probabilistic Inference for Hierarchical Automata Models. International Workshop on Principles of Diagnosis (DX), Murnau, Germany, 2011.

[3] Michael Hofbaur and Martin Sachenbacher: On the Role of Model-based Diagnosis in Functional Safety. International Workshop on Principles of Diagnosis (DX), Jerusalem, Israel, 2013.