Formalisierung von Verhaltensdifferenzen in Automatisierungssoftware
| Forschungsthema: | Regression Verification |
|---|---|
| Typ: | BA |
| Datum: | 2015-08-05 |
| Betreuer: |
Mattias Ulbrich Alexander Weigl |
| Aushang: |
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