Policy iteration for value set analysis of PLC programs

Völker, Marcus; Kowalewski, Stefan (Thesis advisor); Beckert, Bernhard (Thesis advisor)

Aachen : RWTH Aachen University (2023)
Buch, Doktorarbeit

In: Aachener Informatik-Berichte (AIB) 2023,01
Seite(n)/Artikel-Nr.: 1 Online-Ressource : Illustrationen, Diagramme

Dissertation, RWTH Aachen University, 2023

Kurzfassung

Die Gewährleistung korrekten Verhaltens von Computersystemen ist eine wichtige Aufgabe, um Gefahren von ihren Benutzern abzuwenden. Zu diesem Zweck wurden zahlreiche Analysetechniken entwickelt, mit denen Fehler in Software gefunden werden können oder bewiesen werden kann, dass die Software einer bestimmten Spezifikation korrekten Verhaltens entspricht. Eine dieser Techniken ist die Wertebereichsanalyse (VSA), mit der eine Abschätzung der Werte der Programmvariablen an jedem Punkt des Programms ermittelt werden kann. Mithilfe dieser können viele Fehler gefunden werden, wie z. B. Division durch Null, illegaler Speicherzugriff, oder unerreichbarer Code. Während die Wertbereichsanalyse klassischerweise mittels Kleene-Iteration durchgeführt wird, wurde in den letzten Jahren ein anderer Ansatz namens Policy-Iteration entwickelt, der das Potenzial hat, ähnliche oder bessere Ergebnisse in kürzerer Zeit zu erzielen. Bei der Policy-Iteration wird eine Heuristik verwendet, um das Programm erst auf eine bestimmte Weise zu vereinfachen, dann die Wertemengen dieses vereinfachten Programms zu finden und dann zu prüfen, ob das Ergebnis auf das ursprüngliche Programm anwendbar ist. Wenn ja, wird das Ergebnis verwendet, andernfalls müssen verschiedene andere Vereinfachungen geprüft werden, bis ein brauchbares Ergebnis gefunden wird. Da es sich bei der Policy-Iteration um einen heuristischen Algorithmus handelt, macht er bestimmte Annahmen über das Programmverhalten, um gute Ergebnisse zu erzielen. Es stellt sich jedoch heraus, dass diese Annahmen nicht garantiert werden können, wenn das Programm Fehler enthält. Da Programmanalyse genutzt wird, um Fehler zu finden, ist die Annahme eines fehlerfreien Programms nicht allgemeingültig. In dieser Arbeit zeigen wir mehrere Möglichkeiten auf, die Heuristik aus der Literatur zu verbessern, indem wir Programmschleifen betrachten. Zunächst stellen wir eine Möglichkeit vor, mit Hilfe einer Voranalyse bestimmtes Verhalten von Schleifen zu bestimmen, und verwenden diese Informationen, um eine Heuristik zu erstellen, die in vielen Fällen zu genaueren Lösungen führt als die Standardheuristik. Dies geschieht auf Kosten der zusätzlichen Laufzeit, die zur Durchführung dieser Voranalyse erforderlich ist. Danach zeigen wir eine Möglichkeit, Verzweigungen in zyklischem Code—typisch für reaktive Systeme—als Schleifen zu betrachten. Auf diese Weise können wir unsere Schleifenheuristik auf eine breitere Auswahl von Programmen anwenden, auch wenn höhere Zeitkosten dafür sorgen, dass sie nur in bestimmten Fällen nützlich ist. Anschließend zeigen wir, wie die Voranalyse entfernt werden kann, um uns an die Laufzeit der ursprünglichen Policy-Iteration anzunähern, wobei ähnlich gute Ergebnisse wie bei der zuvor eingeführten teuren Version erzielt werden. Dies hat den zusätzlichen Vorteil, dass die Algorithmen wie beim zweiten Ansatz auf Verzweigungen angewendet werden können, ohne dass zusätzliche Kosten anfallen. Wir begründen, dass dies die Version der Policy-Iteration ist, die im Allgemeinen mit einer umfassenden Bewertung der generierten Programme verwendet werden sollte. Schließlich zeigen wir einen Weg, polynomielle Ungleichungen zu analysieren, indem wir sie als Konjunktionen von einfacheren Ungleichungen umdeuten. Dadurch können wir nicht nur die Ergebnisse der Wertebereichsanalyse für Programme mit solchen Ungleichungen verbessern, sondern diese Programme auch für die Policy-Iteration zugänglich machen.

Einrichtungen

• Fachgruppe Informatik [120000]
• Lehrstuhl für Informatik 11 (Embedded Software) [122810]