SCADE Design Verifier against Z3: Who will catch the bug first?
Modelltransformation SCADE Suite -> UPPAAL
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
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
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.:
Geforderte Kompetenzen
Bearbeitung
Betreuer
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:
Geforderte Kompetenzen
Interesse für Bahntechnik, Modellierung und formale Methoden.
Modellbasierte Entwicklung mit Java im Eclipse-Kontext.
Beginn
Sofort
Betreuer