Effizienter Umgang mit Zeitkonstanten in der Verifikation reaktiver Systeme
| Forschungsthema: | Improve APS, PLC Verification |
|---|---|
| Typ: | MA |
| Datum: | 2017-07-14 |
| Betreuer: |
Mattias Ulbrich Alexander Weigl |
| Aushang: |
Effizienter Umgang mit Zeitkonstanten in der Verifikation reaktiver Systeme
Hintergrund
Automatisierte Produktionsanlagen sind häufig mehrere Jahrzehnte lang im Einsatz und erfüllen sicherheitskritische Aufgaben. Deshalb sind Fehler im Code nach Möglichkeit zu vermeiden. Wir forschen deshalb an Methoden und Techniken zur formalen Verifikation von Anlagensoftware.
Bei der Verifikation von Software für Automatisierungsanlagen – wie auch bei der für andere Arten von reaktiven Systemen – spielen Zeitkonstanten eine nicht unerhebliche Rolle: Bei Steuersoftware, die technische Systeme antreibt, wird damit der Physik der Anlage Zeit eingeräumt, das erstrebte Ergebnis zu erreichen, bevor der nächste Schritt eingeleitet wird.
Große Zeitkonstanten haben einen großen Nachteil für die formale Verifikation: Die benötigten Wartezyklen verlängern die zu untersuchenden Eingabeströme unnötig. Wartet eine Anlage an einer Stelle im Programm 1000 Schritte, bis sie fortfährt, so ist es naheliegend, dass zumindest alle Ein-/Ausgabefolgen der Länge 1000 betrachtet werden müssen, um Ergebnisse erzielen zu können.
Aufgabe
Ihre Aufgabe bei dieser Arbeit ist es, Verfahren zu entwickeln, bei denen von den konkreten Zeitkonstanten in reaktiven Systemen abstrahiert wird, um den Suchraum der formalen Verifikation kleiner zu machen. Dazu sollen zunächst verschiedene verwandte Verfahren aus der Literatur recherchiert werden (Zeitregionen bei Timed Automata, symbolische Abstraktion), und untersucht werden, wie diese sich auf die Verifikation reaktiver Systeme übertragen lassen. Ein Ansatz soll ausgearbeitet werden, seine Korrektheit untersucht, und (falls es die Zeit zulässt) prototypisch umgesetzt werden.
Anforderungen
- Interesse an Formalen Systemen, Automatenmodellen
- Offenheit gegenüber einer theoretischen Arbeit
- Kenntnisse, die in der VL Formale Systeme (o.ä.) vermittelt werden.
Kontakt und Betreuung
- Dr. Mattias Ulbrich (Raum 229, Geb. 50.34)
- Alexander Weigl (Raum 225, Geb. 50.34)