Symbolic methods for formal verification of industrial control software

Bohlender, Dimitri; Kowalewski, Stefan; Hermanns, Holger

doi:40884

Symbolic methods for formal verification of industrial control software = Symbolische Methoden zur formalen Verifikation von industrieller Steuerungssoftware

Bohlender, Dimitri^RWTH*

2021 & 2022

Verantwortlichkeitsangabevorgelegt von Dimitri Bohlender, M.Sc. RWTH

ImpressumAachen : RWTH Aachen University 2021

Umfang1 Online-Ressource : Illustrationen, Diagramme

ReiheAachener Informatik-Berichte ; 2021-11

Dissertation, RWTH Aachen University, 2021

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University 2022

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Kowalewski, Stefan (Thesis advisor) ; Hermanns, Holger (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2021-09-23

Online
DOI: 10.18154/RWTH-2021-10633
URL: https://publications.rwth-aachen.de/record/835546/files/835546.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
constrained Horn clauses (frei) ; formal methods (frei) ; formal verification (frei) ; model checking (frei) ; programmable logic controller (frei) ; symbolic methods (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Viele der Systeme, auf die wir uns verlassen und mit denen wir täglich interagieren, sind softwaregesteuert. Jedoch ist die fehlerfreie Implementierung solcher Systeme schwer, da hierfür die enorme Menge an erreichbaren Systemzuständen von den Entwicklern berücksichtigt werden muss. Während Testen der gängige Ansatz zur Qualitätssicherung ist, können damit nur Fehler gefunden, aber nicht deren Abwesenheit gezeigt werden. Im Gegensatz dazu haben formale Methoden eine mathematische Basis und ermöglichen die rigorose Überprüfung von formal beschriebenem Systemverhalten. Insbesondere bringen sie Verfahren zur formalen Verifikation hervor, mit denen sich untersuchen lässt, ob ein System bestimmte Spezifikationen einhält. Obwohl solche Verfahren vereinfacht als automatische Erkundung des Zustandsraums eines Systems verstanden werden können, ist die explizite Aufzählung jedes erreichbaren Zustands oft vermeidbar. Hierzu operieren symbolische Methoden auf vielen Zuständen gleichzeitig, indem sie Zustandsmengen und Übergangsrelationen als logische Formeln repräsentieren. Diese Arbeit befasst sich mit symbolischen Methoden zur formalen Verifikation der softwaregesteuerten reaktiven Systeme, die in industriellen Steuerungsanwendungen verwendet werden. Während diese Systeme oft in einem sicherheitskritischen Umfeld betrieben werden, erschweren die Spezifikationen und Eigenheiten der Domäne die Verwendung existierender Verifikationswerkzeuge und schaffen Bedarf an computergestützten Verfahren zur Analyse des Systemverhaltens. Unsere Beiträge behandeln diese Problematik auf eine plattformunabhängige Art und Weise, werden aber am Beispiel von speicherprogrammierbaren Steuerungen präsentiert, welche auf die Anforderungen der industriellen Automatisierung zugeschnitten und entsprechend weit verbreitet sind: (i) Wir stellen eine Prozedur zur beschränkten Verifikation von Steuerungssoftware vor, deren Schranke anstatt der Einschränkung der Länge von Anweisungsfolgen die Anzahl der Programmausführungszyklen bezeichnet. Indem wir die am Ende eines Zyklus erreichbaren Zustände in Relation setzen, ermöglichen wir die Überprüfung von Spezifikationen, die sich nur auf die beobachtbaren Zustände beziehen. (ii) Wir leiten eine logische Charakterisierung von Steuerungssoftware-Sicherheit in Form von Horn-Klauseln aus Grundlagen der Sicherheit reaktiver Systeme ab und zeigen, dass dieser Ansatz konkurrenzfähig ist. Um die Modularität von Steuerungssoftware auszunutzen, erweitern und kombinieren wir die Charakterisierung mit einer domänenspezifischen Analyse zur Approximation des Zustandsraums. (iii) Wir geben ein Verfahren zur Verifikation der Einhaltung der automatenbasierten Spezifikationen des PLCopen an. Im Gegensatz zu verwandten Arbeiten behandelt es Aufrufe originalgetreu, ist inkrementell und nutzt das Lösen von Horn-Klauseln. (iv) Wir präsentieren Techniken zum Entwurf und zur Verifikation von Steuerungssoftware, die robust gegenüber Neustarts sein soll. Im Unterschied zu früheren Arbeiten wird die Programmsemantik nicht überapproximiert, um falsch-positive Resultate zu vermeiden. Zudem zeigen wir, wie die Wahl persistenter Variablen auf Parametersynthese reduziert und mit den vorhergehenden Techniken gelöst werden kann.

Many of the systems that we rely on, and interact with on a daily basis, are driven by software. Unfortunately, design and implementation of such systems is naturally prone to error, as it is done by humans and involves reasoning about the vast number of states a system may reach. While testing is the common approach to alleviating the risk of writing faulty software, it can only help with finding errors, but not prove their absence. By way of contrast, formal methods have mathematical foundations, and enable rigorous reasoning about the behaviour of formally modelled systems. In particular, they give rise to formal verification procedures for proving a system's compliance with certain formal specifications. Although many such procedures can simplistically be thought of as an automatic exploration of a system's state space, the explicit enumeration of each reachable state can often be avoided. To this end, symbolic methods reason about many states at a time, by representing sets of states and transition relations as logical formulas. This thesis is concerned with advances in symbolic methods for formal verification of the software-driven reactive systems that are used in the setting of industrial automation. While these systems often operate in safety-critical environments, the specifications and peculiarities of the domain impede the use of existing verification machinery for general-purpose programming languages, leaving engineers in need of computer-aided reasoning about the control software semantics. Our contributions address this issue in platform-agnostic ways, but are presented using the example of programmable logic controllers which are tailored to the industrial automation domain and therefore widely used: (i) We propose a procedure for bounded verification of control software, where the bound denotes the number of program execution cycles instead of the traditional restriction of the number of instructions. By relating the states that are reachable at the end of each cycle through a dynamic and incremental encoding, we enable checking specifications that only refer to these observable states, while performing on par with state of the art. (ii) We derive a logical characterisation of control software safety in terms of constrained Horn clauses from reactive systems safety foundations. Leveraging solvers for this formalism is shown to be competitive with state-of-the-art approaches. To exploit the modularity of control software, the characterisation is also extended and combined with mode abstraction -- a domain-specific analysis for approximating the state space. (iii) We state a procedure for proving a module's compliance with the automaton-based specifications used by PLCopen. Unlike previous work, our approach handles calls faithfully, is incremental, compositional, and leverages Horn clause solving. (iv) We present approaches for the design and verification of control software that is resilient to potential restarts of the controller. In contrast to previous work, we do not over-approximate the program semantics and get false positives, but reason about the precise program semantics by reducing the problem to satisfiability of Horn clauses. We show how the choice of persistent variables can be reduced to parameter synthesis, and solved by extending the previous verification procedures.

OpenAccess:
PDF
(additional files)