Norbert Völker: Ein Rahmen zur Verifikation von SPS-Funktionsbausteinen in HOL.
Dissertation unter der Leitung von Prof. Dr.-Ing. Bernd J. Krämer  am Lehrgebiet Datenverarbeitungstechnik des Fachbereichs Elektrotechnik, FernUniversität Hagen, August 1998.
Veröffentlicht im Shaker Verlag, Aachen, 1998, ISBN 3-8265-4367-X, ISSN 0945-0718.

Zusammenfassung

Aufgrund der höheren Flexibilität werden in der Automatisierungstechnik mehr und mehr Steuerungsalgorithmen in der Form speicherprogrammierbarer Steuerungen (SPS) als Software realisiert. Die in der Praxis vorherrschende Methode zur Überprüfung der Funktionalität, Korrektheit und funktionalen Sicherheit von SPS-Programmen bildet der Test des zu steuernden Systems, häufig anhand einer Simulation der Einsatzumgebung. Diese Vorgehensweise weist aber den prinzipiellen Mangel auf, daß für die meisten Programmen nur eine relativ kleine Teilmenge des möglichen Systemverhaltens überprüft werden kann.

Als ergänzende Maßnahme im Softwareentwicklungsprozeß bietet sich die formale Verifikation an, bei der die Anforderungen an ein Programm formalisiert und mit mathematischer Strenge nachgewiesen werden. Im Gegensatz zur Methode des Testens werden hierbei alle mögliche Abläufe des Systems berücksichtigt. Aufgrund des erheblichen Aufwands bei der formalen Spezifikation  der Programmeigenschaften und bei der Durchführung der Beweise empfiehlt es sich, die Verifikation mit maschineller Hilfe durchzuführen. Darüberhinaus sind Beweistechniken zu bestimmen, die es erlauben, auf nachgewiesenen Eigenschaften der Grundbausteine einer Anwendung aufzubauen.

Der Hauptgegenstand dieser Dissertation ist die Konstruktion eines Rahmen für die maschinengestützte Verifikation von SPS-Funktionsbausteinen auf der Grundlage der Prädikatenlogik höherer Ordnung (engl.: higher order logic, HOL). Dieser Rahmen wurde in Form von Theorien der Objektlogik HOL des generischen Beweisunterstützungssystems Isabelle implementiert. Dazu wurden eine Programmiersprache ST- sowie die temporale Logik LTL (Linear Time Logic) in HOL eingebettet. Die gewählte Sprache ST- ist eine Teilmenge der in der IEC-Norm 61131-3 standardisierten SPS-Programmiersprache Strukturierter Text (ST). Als Nebeneffekt wurde für die in ST- enthaltenen Sprachkonstrukte eine formale Semantik angegeben.

Die Einbettung der Programmiersprache ST- wäre ohne eine Theorie von Datentypen in HOL kaum  öglich gewesen. Ein erheblicher Teil dieser Arbeit befaßt sich daher mit der Entwicklung eines Datentyppakets für HOL. Es automatisiert das Zufügen neuer Datentypen zu einer Theorie durch eine konservative, rein definitorische Theorieerweiterung. Auf diesem Fundament wird dann die Einbettung von ST- in HOL definiert. Die Anwendbarkeit des so konstruierten HOL-Rahmens zur Verifikation wird am Beispiel einer einfachen Ampelsteuerung demonstriert.

Summary

The flexibility of software has the effect that more and more control algorithms in the automation area are implemented as programmable logic controllers (PLCs). In industry, the functionality and safety of PLC-programs is checked predominantly by system tests performed in a simulated hardware environment. The principal deficiency of this method is that only a relatively small subset of the possible behaviour of most application programs can be examined.

This observation suggests the use of formal verification as a supplementary measure in the software development process. With this method the requirements of control programs are formalised and proven with mathematical rigour. In contrast to the method of testing, this approach takes all possible runs of a system into account. As the process of formalisation and the proofs involve a considerable amount of effort and work, it is essential to perform the verification task with mechanical support. Furthermore it is important to develop proof techniques that simplify proofs of complex programs by reusing proven properties of base components.

The work described in this dissertation establishes a foundation for the machine supported verification of PLC function blocks. The approach is based on higher order predicate logic (HOL) and has been implemented in the form of theories of the HOL object logic of the Isabelle generic theorem proving assistant. In the course of this work, a programming language, called ST-, and linear time temporal logic (LTL) were embedded in HOL. The language ST- is essentially a subset of the PLC programming language Structured Text (ST) standardised in the IEC standard 61131-3. As a welcome side effect, this embedding provides a formal semantics for those constructs of ST contained in ST-.

An embedding of the programming language ST- without a theory of data types is hardly conceivable. A substantial part of this dissertation therefore deals with the development of a HOL data type package that implements the addition of new data types to HOL by a conservative, purely definitional theory extension. On this basis, the embedding of ST- in HOL is constructed. The applicability of the verification framework proposed is demonstrated with the example of a simple traffic light controller.

Back to homepage