guest ::
Policy iteration for value set analysis of PLC programs
2023
Dissertation, RWTH Aachen University, 2023
Veröffentlicht auf dem Publikationsserver der RWTH Aachen University
Genehmigende Fakultät
Fak01
Hauptberichter/Gutachter
;
Tag der mündlichen Prüfung/Habilitation
2023-03-06
Online
DOI: 10.18154/RWTH-2023-04281
URL: https://publications.rwth-aachen.de/record/956653/files/956653.pdf
Einrichtungen
Thematische Einordnung (Klassifikation)
DDC: 004
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.Ensuring the correct behaviour of computing systems is an important task to prevent danger to the users of such systems. To do this, many analysis techniques have been developed that can find bugs in software, or prove that it complies to some specification of correct behaviour. Among these techniques, a fundamental analysis is value set analysis (VSA), which can determine an approximation of the program variables' values at each point of the program. This is very important information, as many faulty behaviours can be traced back to variables taking unexpected values, such as division by zero, access to uninitialised memory or outside a buffer, or unreachable code. While classically, value set analysis is performed with the algorithm of Kleene iteration, another approach called policy iteration has been developed in recent years that provides an alternative with the potential of finding similar or better results than Kleene iteration in less time. Policy iteration works by using a heuristic to simplify the program in a certain way, finding the value sets of that program, and then checking whether the result is applicable to the original program. If yes, the results are used, otherwise different simplifications have to be checked, until a usable result is found. As policy iteration is a heuristic algorithm, it makes certain assumptions about program behaviour in order to achieve good results. It turns out, however, that these assumptions are not guaranteed if the program contains errors which cause it to behave differently than expected. As we use program analysis to find errors such as this, assuming an error-free program is not necessarily a good assumption. In this thesis, we show several ways to improve the original heuristic by focusing on program loops. First, we present a way to use a pre-analysis to determine some aspect of the loops' behaviours, and use this information in order to build a heuristic that leads to more accurate solutions than the standard heuristic in many cases, at the cost of additional running time necessary to perform this pre-analysis. Then, we show a way to reinterpret branches as loops if they occur in cyclical code, which is typical for programs in reactive systems, such as the systems used for factory automation. This allows us to use our loop heuristic on a wider variety of programs, even though the cost becomes even greater, and it is useful only in specific cases. Afterwards, we show how to remove the pre-analysis to gain back the lost time, while still retaining similarly good results to the expensive version introduced before. This has the additional benefit of allowing usage of the algorithms on branches as in the second approach, without incurring any additional costs. We motivate that this is the version of policy iteration that should be used in general with an extensive evaluation of generated programs. Finally, we show a way to analyse polynomial inequalities with value set analysis by reinterpreting them as conjunctions of simpler inequalities. This not only allows us to improve value set analysis results on programs that feature such inequalities, but also makes these programs accessible to policy iteration.
OpenAccess: 
PDF
(additional files)
Dokumenttyp
Dissertation / PhD Thesis/Book
Format
online
Sprache
English
Externe Identnummern
HBZ: HT030012666
Interne Identnummern
RWTH-2023-04281
Datensatz-ID: 956653
Beteiligte Länder
Germany
|
The record appears in these collections: |