S7 Simulator für [mc]square

Motivation

An unserem Lehrstuhl wird der Model-Checker [mc]square entwickelt, der zur Verifikation von Programmen eingebetteter Systeme genutzt werden kann. Zu den unterstützten Plattformen gehören verschiedene Microkontroller aber auch Speicherprogrammierbare Steuerungen (SPSen), welche zur Steuerung und Regelung von großtechnischen Anlagen und Maschinen verwendet werden. Durch die häufige Verwendung in sicherheitskritischen Umfeldern ist die Verifikation der Programme in besonderem Maße sinnvoll oder sogar vorgeschrieben. Andererseits ermöglicht die recht einfache Funktionsweise der SPSen eine formale Überprüfung vieler Programme.

Zur Programmierung von SPSen können unterschiedliche Sprachen verwendet werden. Für die Sprache Anweisungsliste (AWL) gibt es bereits einen Simulator, mithilfe dessen das Modell zur Verifikation von SPS-Programmen erstellt wird. Dieser Simulator ist modular geschrieben, so dass er einfach auf unterschiedliche Eingabesprachen für SPS-Programme angepasst werden kann.

Aufgabenstellung

Der vorhandene Simulator soll um die Sprache Statement List (STL) ergänzt werden. STL wird zur Programmierung von Siemens Simatic S7 SPSen verwendet und ist dabei wie AWL eine Assembler-ähnliche Sprache, die aus einem Textformat eingelesen wird.

Im Rahmen der Arbeit soll ein Parser geschrieben werden, der STL-Programme einliest und die simulierte Hardware entsprechend konfiguriert. Ziel ist es dann, den vorhandenen Simulator anzupassen und zu ergänzen, so dass auch die Überprüfung von STL-Programmen möglich wird.

Vorkenntnisse

Hilfreiche, aber nicht notwendige Vorkenntnisse sind:

  • Java
  • Eingebettete Systeme

Betreuer

Diese Website verwendet Cookies. Durch die Nutzung der Website stimmen Sie dem Speichern von Cookies auf Ihrem Computer zu. Wenn Sie nicht einverstanden sind, verlassen Sie bitte die Website.Weitere Information

RWTH Aachen - Lehrstuhl Informatik 11 - Ahornstr. 55 - 52074 Aachen - Deutschland