zurück zur Startseite der Softwaretechnik-Trends , zu Band 19 Heft 3

Dissertationen


Norbert Völker: Ein Rahmen zur Verifikation von SPS-Funktionsbausteinen in HOL (Shaker Verlag 1998, ISBN: 3-8265-4367-X)


1. Referent: Prof. Dr.-Ing. Bernd Krämer
2. Referent: Prof. Dr. L. Trybus, Rzeszów, Polen

Datum der Prüfung: 28. August 1998


Zusammenfassung:

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 mö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.



zurück zur Startseite der Softwaretechnik-Trends , zu Band 19 Heft 3