Konformanz von Testtabellen mittels Hornklauseln

Typ:	BA / MA
Datum:	2019-03-13
Betreuer:	Alexander Weigl
Aushang:	PDF

Hintergrund

Am Lehrstuhl wurden die Generalisierten Testtabellen, eine verständliche tabellenbasierte Spezifikationssprache entwickelt. Eine Generalisierte Testtabelle ist dabei ein zustandsbasierter Vertrag mit Vor- und Nachbedingungen, dabei hängen die aktuellen Bedingungen von einem implizierten Zustand ab. Diese Art von Spezifikationssprachen findet dabei Einsatz bei Reaktiven Systemen, also solche Systeme, die die Umgebung überwachen und auf Änderungen reagieren. Reaktive Systeme finden Einsatz in der Robotik, IoE oder automatisierten Produktionsanlagen.

Ihre Aufgabe

Bisher wurde die Einhaltung eines Reaktiven Systems mit einem Model Checker (nuXmv) überprüft. Ihre Aufgabe ist nun das bisherige Verfahren auf Löser für Hornklauseln zu adaptieren. Dazu müssen Sie zum einen die Tabellen in Hornklauseln überführen, zum Anderen die Programme in Hornklausel encodieren.

Ihr Profil

Programmierkenntnisse in Java oder Kotlin verpflichtend. Weiterhin sollten Sie ein starkes Interesse für Formale Methoden, Temporale Logiken und Automatentheorie mitbringen. Sie sollten die Veranstaltung Formale System (oder Äquivalentes) bestanden haben.

References

1. Horn Clause Solving for Program Verification; N. Bjorner et.al.

2. Bohlender, D. and Kowalewski, S., "Compositional Verification of PLC Software using Horn Clauses and Mode Abstraction", IFAC-PapersOnLine, vol. 51, iss. 7, pp. 428-433, 2018