Formalisierung von Verhaltensdifferenzen in Automatisierungssoftware

Forschungsthema:Regression Verification
Typ: DA / BA / MA
Datum: 2015-08-05
Betreuer: Mattias Ulbrich
Alexander Weigl
Bearbeiter: Kevin Zhang
Aushang: PDF

Hintergrund

Sequential Function Chart (SFC) ist eine grafische Programmiersprache, die häufig für die Programmierung von automatisierten Industrieanlagen Verwendung findet. SFCs beschreiben Verhalten als endliche Automaten durch Bedingungen an Zustandsübergängen und Zuweisungen zu bestimmten Ereignissen. Industrieanlagen sind auf eine lange Lebensdauer ausgelegt (>30 Jahre). Eine Differenz im Verhalten der Fabrikanlage während durch eine Softwareevolution muss bei einer ordnungsgemäßen Implementierung die Beschreibung durch die Anforderungdokumente gedeckt sein.

Ziel

Sie entwickeln und untersuchen Methoden zum Finden der Unterschiede im Verhalten zwischen zwei SFCs. Die gefundene Differenz soll kompakt aber exakt durch eine logische Formel beschrieben werden und als Eingabe für unsere Werkzeuge zur Regressionsverifikation (Äquivalenzcheck zwischen Softwareversionen) dienen.

Voraussetzungen

Grundlegende Kenntnisse in Logik, z. B. durch die Vorlesung “Formale Systeme”, Automatentheorie

Kontakt:

  • Dr. Mattias Ulbrich (50.34R229), ulbrich@kit.edu
  • Alexander Weigl (50.34R225), weigl@kit.edu