SCADE Design Verifier against Z3: Who will catch the bug first?

Modelltransformation SCADE Suite -> UPPAAL

Instanziierung von Anlagenmodellen für die Diagnose von Bahnsicherungsanlagen

Regelbasierte Evaluierung von System-Zustandsabbildern für die Diagnose von Bahnsicherungsanlagen

SCADE Design Verifier against Z3:

Who will catch the bug first?

Problemstellung und Zielsetzung

Die SCADE Tool Suite ist eine umfangreiche, kommerzielle Entwicklungsumgebung für sicherheitskritische Systeme von Esterel Technologies basierend auf der synchronen Sprache Scade. In der Arbeitsgruppe „Grundlagen der Informatik“ wurden bereits einige Fallstudien in SCADE modelliert, zum Teil in Kooperation mit einem Industriepartner. Zur formalen Verifikation verwendet die SCADE Suite den Design Verifier. In dieser Arbeit soll das Verhalten des Design Verifiers mit dem bei Microsoft entwickelten Z3, einem alternativen SAT-Solver basierten Modelchecker, verglichen werden. Um die existierenden Fallstudien in Z3 zu importieren, soll eine Modelltransformation von Scade in die Eingabesprache von Z3 konzipiert und realisiert werden. Im nächsten Schritt sollen die beiden Modelchecker Design Verifier und Z3 anhand der Fallstudien in Bezug die Anwendung von Built-In Heuristiken zur Effizienzsteigung miteinander verglichen werden. Ein Compilerfrontend für Scade kann vermutlich aus einer früheren studentischen Arbeit übernommen werden. Publikationen zu beiden Model Checkern und ihren Eingabeformaten als auch zu den Konzepten einer Übersetzung von einer synchronen Sprache in Z3 stehen zur Verfügung. Der Umfang dieses Vergleichs wird der angestrebten Arbeit angepasst.

Geforderte Kompetenzen

Kenntnisse der SCADE Suite und Compilerbau sind hilfreich.

Beginn

Sofort

Betreuer

Michaela Huhn

Modelltransformation

SCADE Suite -> UPPAAL

Problemstellung und Zielsetzung

Die SCADE Tool Suite ist eine umfangreiche, kommerzielle Entwicklungsumgebung für sicherheitskritische Systeme von Esterel Technologies basierend auf der synchronen Sprache Scade. In der Arbeitsgruppe „Grundlagen der Informatik“ wurden bereits einige Fallstudien in SCADE modelliert, zum Teil in Kooperation mit einem Industriepartner. Zur formalen Verifikation verwendet die SCADE Suite den Design Verifier.

UPPAAL ist ebenfalls ein Tool zur Verifikation von Modellen von Echtzeit-Systemen. Hierzu werden sogenannte Timed Automata verwendet. In der Arbeitsgruppe wurden bereits einige Untersuchungen durchgeführt, wie eine Modelltransformation von SCADE zu UPPAAL theoretisch erfolgen könnte.

Ziel dieser Arbeit soll die Erstellung einer automatischen Transformation eines SCADE Modells in ein UPPAAL Modell sein. Dazu soll zunächst eine Klassifikation der SCADE Elemente erfolgen, die transformiert werden sollen. Anschließend ist es von Nöten, Zeitbegriffe genau zu definieren. Hierzu ist es wichtig festzulegen, was man genau unter Zeitvariablen und –konstanten in SCADE und UPPAAL versteht. Vor der Implementierung ist zu klären, ob gegebenenfalls Module, wie beispielsweise ein Compilerfrontend, aus anderen Projekten wiederverwendet werden können.

Geforderte Kompetenzen

Kenntnisse der SCADE Suite und Compilerbau sind hilfreich.

Beginn

Sofort

Betreuer

Sara Bessling

Instanziierung von Anlagenmodellen für die
Diagnose von Bahnsicherungsanlagen

Problemstellung

Bei Bahnautomatisierungsanlagen erfordert die Systemgröße und  -komplexität eine automatisierte Ausführung von Diagnose- und Überwachungsaufgaben, um Fehler möglichst früh erkennen, lokalisieren und schnell beheben zu können, und somit eine hohe Systemverfügbarkeit zu gewährleisten. Die Durchführung dieser Aufgaben setzt  eine breite Wissensbasis über die funktionalen und strukturellen Zusammenhänge des Zielsystems voraus. Dieses Diagnosewissen kann von Fachleuten bereitgestellt und durch im Betrieb gesammelte Erfahrung ergänzt werden.

Bei unserem Industriepartner wird das Störungsverhalten einzelner  Komponenten von Bahnanlagen und anderen bahnrelevanten Systemen in sogenannten Störungskatalogen erfasst. Ein formales Modell beschreibt die durch Fehler initiierte Ausbreitung und Wandlung von Symptomen bis zu dem Punkt, an dem die Auswirkungen für einen externen Beobachter bzw. ein angeschlossenes Diagnosesystem sichtbar werden. Eine modellbasierte Diagnose interpretiert Systemzustände und -ereignisse und leitet daraus konkrete Handlungsanweisungen ab.

Zielsetzung und Aufgaben

Bahnanlagen werden jeweils individuell projektiert und konfiguriert. Dementsprechend müssen für eine Anlagendiagnose anlagenspezifische Systemmodelle aus den bereits erstellten Komponententyp-modellen und Informationen über Komponentenabhängigkeiten instanziiert werden. In dieser Arbeit soll die Methodik für diese Modellinstanziierung ausgearbeitet werden.

Die Aufgabe umfasst:

• Analyse der Anforderungen und benötigten Informationen für eine Instanziierung
• Bestimmung der benötigten Modellierungskonzepte für Anlagen¬instanzmodelle
• Ergänzung eines existierenden Metamodells des Störungskatalogs um neue Konzepte
• Bereitstellung von Softwarewerkzeugen zur Erzeugung, Bearbeitung und Transformation von Instanzmodellen

Geforderte Kompetenzen

Interesse für Bahntechnik, Modellierung und formale Methoden.
Modellbasierte Entwicklung mit Java im Eclipse-Kontext.

Beginn

Sofort

Betreuer

Dennis Klar

Michaela Huhn

Regelbasierte Evaluierung von
System-Zustandsabbildern für die
Diagnose von Bahnsicherungsanlagen

Problemstellung

Bei Bahnautomatisierungsanlagen erfordert die Systemgröße und  -komplexität eine automatisierte Ausführung von Diagnose- und Überwachungsaufgaben, um Fehler möglichst früh erkennen, lokalisieren und schnell beheben zu können, und somit eine hohe Systemverfügbarkeit zu gewährleisten. Die Durchführung dieser Aufgaben setzt  eine breite Wissensbasis über die funktionalen und strukturellen Zusammenhänge des Zielsystems voraus. Dieses Diagnosewissen kann von Fachleuten bereitgestellt und durch im Betrieb gesammelte Erfahrung ergänzt werden.

Bei unserem Industriepartner wird das Störungsverhalten einzelner  Komponenten von Bahnanlagen und anderen bahnrelevanten Systemen in sogenannten Störungskatalogen erfasst. Ein formales Modell beschreibt die durch Fehler initiierte Ausbreitung und Wandlung von Symptomen bis zu dem Punkt, an dem die Auswirkungen für einen externen Beobachter bzw. ein angeschlossenes Diagnosesystem sichtbar werden. Eine modellbasierte Diagnose interpretiert Systemzustände und -ereignisse und leitet daraus konkrete Handlungsanweisungen ab.

Zielsetzung und Aufgaben

Zur technischen Integration einer modellbasierten Laufzeit-Diagnose ist eine mehrstufige, bidirektionale Übersetzung zwischen dem zu diagnostizierenden Zielsystem und dem Diagnosemodell der Anlage  erforderlich: Während im Zielsystem Nachrichten mit Fehlercodes von Komponenten eintreffen, die sich über ihre physikalische Adresse identifizieren, werden im Diagnosemodell logische Komponenten betrachtet, bei denen Symptome beobachtet und weitergeleitet werden, die Rückschlüsse auf ursächliche Fehler erlauben. Um diese beiden Sichtweisen in Beziehung zu setzen, wird aus den Meldungen unterschiedlicher Form und Herkunft zur Laufzeit zunächst in ein abstraktes Zustandsabbild des Systems aufgebaut. In dieser Arbeit soll nun eine regelbasierte Methodik entworfen werden, die ein solches Zustandsabbild aus Diagnosesicht bewertet (evaluiert) und modellkonforme Symptome ableitet.


Die Aufgabe umfasst:

• Analyse der verfügbaren Daten und Möglichkeiten zur automatisierten Auswertung von Zustandsabbildern
• Definition einer Sprache (in textueller Syntax) zur Beschreibung von Evaluierungsregeln
• Ergänzung eines existierenden Metamodells um neue Modellierungskonzepte
• Bereitstellung von Softwarewerkzeugen zur Definition von Regeln und zur Ausführung einer kontinuierlichen Evaluation eines Zustandsabbilds

Geforderte Kompetenzen

Interesse für Bahntechnik, Modellierung und formale Methoden.
Modellbasierte Entwicklung mit Java im Eclipse-Kontext.

Beginn

Sofort

Betreuer

Dennis Klar

Michaela Huhn