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

Modelltransformation SCADE Suite -> UPPAAL

Erstellung, Einbindung und Visualisierung von Strukturmodellen 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

Erstellung, Einbindung und Visualisierung
von Strukturmodellen für
die Diagnose von Bahnsicherungsanlagen

Ausgangslage und Problemstellung

Bei Bahnautomatisierungsanlagen erfordern 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 kausales 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.

Die bisherige Diagnose-Modellierung setzt konsequent auf das Prinzip der (De-)Komposition: Komplexe Zielsysteme werden in der Analysephase ge-danklich in einfache Betrachtungseinheiten zerlegt. Das Verhalten jeder Einheit wird danach einzeln modelliert. Die Interaktion zwischen den Einheiten wird durch Schnittstellen spezifiziert. Für die spätere Systemdiagnose werden die einzelnen Komponenten dann nach Vorgabe des Systems zusammengesetzt. In der bisherigen Zusammenarbeit wurden umfangreiche Werkzeuge als Eclipse-Plugins zur Modellierung und Modelldatentransformation realisiert.

Zielsetzung und Aufgaben

In der industriellen Praxis hat sich gezeigt, dass die isolierte Betrachtung einer Diagnose-Komponente bisweilen schwierig ist, da der übliche Ver-wendungskontext verloren geht. D.h. der Modellierer wünscht sich häufig, eine Komponente in ihrer typischen Umgebung betrachten zu können.

Zwischen den beiden Extremen (Sicht auf eine einzelne Betrachtungseinheit gegenüber System Engineering Sicht auf das Zielsystem) soll daher eine zusätzliche Modellebene etabliert werden, die sogenannten Strukturmodelle. Ein Strukturmodell beschreibt ein Teilsystem aus dem System Engineering auf der technischen Architekturebene. Es besteht aus einer überschaubaren Anzahl von Komponenten, die für die Diagnose zu betrachten sind. Strukturmodelle sollen auch als „Muster“ dienen, gemäß denen dann ein Diagnosesystem konfiguriert werden muss.

In dieser Arbeit soll der vorhandene Ansatz zur Diagnosemodellierung um die Möglichkeit ergänzt werden, Strukturmodelle zu erstellen und einzubinden.

Die Aufgabe umfasst z.B.:

• Anforderungsanalyse
  
  • was sollen Strukturmodelle leisten?
• Definition eines Metamodells
  
  • welche (neuen) Modellierungskonzepte werden benötigt?
• Definition einer textuellen Eingabesprache
  
  • wie können Strukturdaten erfasst werden?
• Umsetzung einer grafischen Darstellung
  
  • wie können Strukturdaten visualisiert werden?

Geforderte Kompetenzen

• Interesse für Bahntechnik und Modellierung.
• Modellgetriebene Entwicklung mit Java im Eclipse-Kontext.
• Praktische Kenntnisse in EMF, Xtext und Xtend sind hilfreich aber keine Bedingung

Bearbeitung

• als Einzel- oder Teamarbeit
• im engen Kontakt mit unserem Industriepartner
• Beginn: ab 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