Verification of programmable logic controller code using model checking and static analysis

Biallas, Sebastian; Fay, Alexander; Kowalewski, Stefan

doi:HT019148744

Verification of programmable logic controller code using model checking and static analysis = Verifikation von Programmen für speicherprogrammierbare Steuerungen mittels Model-Checking und statischer Analyse

Biallas, Sebastian

2016

VerantwortlichkeitsangabeSebastian Biallas

ImpressumAachen : Shaker Verlag 2016

Umfang1 Online-Ressource (x, 153 Seiten) : Illustrationen, Diagramme

ISBN978-3-8440-4711-0

ReiheAachener Informatik Berichte ; 2016-07

Dissertation, RWTH Aachen University, 2016

Auch veröffentlicht auf dem Publikationsserver der RWTH Aachen University

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Kowalewski, Stefan (Thesis advisor) ; Fay, Alexander (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2016-07-14

Online
URN: urn:nbn:de:hbz:82-rwth-2016-066145
URL: https://publications.rwth-aachen.de/record/668156/files/668156.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
formal verification (frei) ; programmable logic controller (frei) ; model checking (frei) ; static analysis (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Speicherprogrammierbare Steuerungen (SPSen, engl. Programmable Logic Controller) sind Automatisierungsgeräte, welche zur Steuerung, Regelung und Überwachung von industriellen Anlagen und Maschinen eingesetzt werden. Sie besitzen dazu Eingänge, die mit Sensoren verbunden sind, Ausgänge, die mit Aktuatoren verbunden sind und ein Programm, welches die Ausgänge in Abhängigkeit der Eingänge und eines internen Speichers belegt. Da SPSen häufig in kritischen Bereichen eingesetzt werden, in denen eine Fehlfunktion Gefahren für Mensch, Umwelt oder die Anlage bergen kann, ist die Korrektheit des Programms zu prüfen.Diese Dissertation untersucht die formalen Methoden Model-Checking und Statische Analyse, um die Korrektheit von PLC-Programmen zu beweisen. Wir haben dazu das Tool ArcadePLC geschrieben, welches es ermöglicht, diese Techniken vollautomatisch auf PLC-Programme verschiedener Hersteller anzuwenden. Es extrahiert durch abstrakte Simulation ein Modell, welches sämtliches Programmverhalten widerspiegelt. Der Benutzer kann dann überprüfen, ob das Modell einer Spezifikation entspricht, welche er in der Logik CTL formulieren muss oder als Automaten eingegeben kann.Zum Bereich Model-Checking zeigen wir in dieser Dissertation, wie das Modell automatisch abstrahiert werden kann, so dass der Ansatz auch für industrielle Programme skaliert. Es werden dazu zwei verschiedene Abstraktionstechniken eingeführt: Eine durch den Model-Checker gesteuerte Abstraktionsverfeinerung erstellt ein abstrahiertes Modell iterativ durch Analyse von Gegenbeispielen. Außerdem haben wir eine automatische Prädikat-Abstraktion implementiert, welche mithilfe einer SMT-Solvers die formalisierte Programmsematik auf Prädikaten auswertet. Beide Techniken werden anhand verschiedener Programme evaluiert. Weiterhin führen wir einen vereinfachten Spezifkationsformalismus ein, welcher sich an einer in der Industrie etablierten Automatensprache orientiert. Wir implementieren einen Algorithmus, um Programme mit diesem Formalismus zu überprüfen und zeigen, dass durch diese Technik auch Spezifikationsfehler entdeckt werden können. Schließlich zeigen wir noch, wie vom Model-Checker gefundene Gegenbeispiele analysiert werden können, um die eigentlich fehlerhafte Programmzeile automatisch zu lokalisieren.Die von uns implementierte Statische Analyse kann vollautomatisch Programmfehler entdecken. Dazu gehören beispielsweise eine Division durch Null, unerlaubte Array-Zugriffe oder PLC-spezifische Fehler z.B. beim Neustart. Die Analyse basiert auf einer Wertebereichsanalyse, welche eine Übermenge der Werte aller Variablen in allen Programmstellen berechnet. Wir zeigen, wie diese Analyse skalierbar implementiert werden kann. Der Ansatz wird an einer großen industriellen Fallstudie ausgewertet.

Programmable Logic Controllers (PLCs) are control devices used in industry to control, operate and monitor plants, machines and robots. PLCs comprise input connectors, typically connected to sensors, output connectors, typically connected to actuators, and a program, which controls the behavior, computing new output values based on the input values and an internal state. Since PLCs operate in safety-critical environments, where a malfunction could seriously harm the environment, humans, or the plant, it is recommended to verify their programs using formal methods.This dissertation studies the formal methods model checking and static analysis to prove the correctness of PLC programs. For this, we developed the tool Arcade.PLC, which allow the automatic application of these methods to PLC programs written for different vendors. It extracts a model from the program by abstract simulation, which over-approximates the possible program behavior. The user is then able to verify whether the model obeys a specification, which can be written in the logic CTL or using automata. For applying model checking, we demonstrate how the model can be extracted automatically, such that the approach scales to industrial size programs. For this, we introduce two different abstraction techniques: First, we develop an abstraction refinement guided by the model checker that automatically creates an abstracted model by iteratively analyzing counterexamples. Second, we implemented a predicate abstraction that evaluates a formalized program semantics using an SMT solver. Both techniques are evaluated using different programs from industry and academia. Further, we introduce a simplified formalism to write specifications, which is influenced by an automata-based language established in industry. We implement an algorithm to check programs using this formalism and show that this technique is even able to detect errors in the specification. Finally, we detail how counterexamples generated by the model checker can be analyzed automatically to locate the actual erroneous line in the program.The static analysis we developed is able to detect program errors in a fully automatic way. We detect typical errors such as division by zero and illegal array accesses, but also PLC specific errors, e. g., during a restart. The analysis is based on a value-set analysis, which determines the values of all program variables in each program location. These sets are then verified against the predefined checks or user-provided annotations. We show how to implement this analysis such that it scales to industrial size programs. The approach is evaluated on an industrial case study.

OpenAccess:
PDF
(additional files)