+**********************************************************************

*

*

* Einladung

*

*

*

* Informatik-Oberseminar

*

*

*

+**********************************************************************

Zeit: Montag, 06. März 2023, 14:00 Uhr

Ort: Raum 2202 (HBau, 2. Stock), Ahornstr. 55

Hybrid über Zoom: https://rwth.zoom.us/j/99712637671?pwd=U0UzV1JiL1hwWnlzNW5pUC9hVDdOUT09

Referent: Marcus Völker, M.Sc. RWTH

Informatik 11 – Embedded Software

Thema: Policy Iteration for Value Set Analysis of PLC Programs

Abstract:

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.

Es laden ein: die Dozentinnen und Dozenten der Informatik