Konstruktion korrekter Codegeneratoren für Speicherprogrammierbare Steuerungen

Abstract

Zur Entwicklung von Steuerungen werden häufig Modelle eingesetzt. Diese werden mit einem Übersetzer in ein Steuerprogramm übersetzt. Die Korrektheit der Übersetzung wird im Allgemeinen nicht garantiert. Das führt bei sicherheitskritischen Systemen zu einer Lücke bei der Sicherstellung der Korrektheit des Entwicklungsprozesses. Translation Validation schließt diese Lücke durch eine Überprüfung des erzeugten Programms. Diese Arbeit beschäftigt sich mit der Translation Validation realer Steuerungen mit Zeitbedingungen. Um dieses Ziel zu erreichen, wurde auf das Wissen aus dem Bereich von Zeitsystemen zurückgegriffen, wobei sowohl bestehende Techniken und Datenstrukturen angepasst als auch neue entwickelt wurden. Die vorgestellte Translation Validation erfüllt besondere Anforderungen, die sich durch die Verwendung realer Steuerungen, realer Zeitbedingungen und realer Modelle ergeben. Der komplexen Semantik der vorgegebenen Steuermodelle und -programme wird durch die Verwendung von SPS-Zeitautomaten als einfaches internes Basismodell begegnet. SPS-Zeitautomaten besitzen die Eigenschaften der Steuermodelle und -programme, was ein explizites Modellieren dieser Eigenschaften durch Zwischenzustände unnötig macht. Die Anzahl der Modellzustände und damit die Modellkomplexität steigt während der Translation Validation deshalb nicht zusätzlich an, was die Verarbeitung realer Modellgrößen ermöglicht.

Models are commonly used in controller development. A control program is generated by a compiler. In general the correctness of the compilation process is not assured. Especially for safety-critical systems this leads to a gap in the correctness of the development process. Translation Validation closes this gap by validation of the generated control program. This thesis applies the method of Translation Validation to real-world controllers with time conditions. For this purpose known methods and data structures from the scientific field of timed models were adapted and new ones created. The Translation Validation presented satisfies the requirements demanded by real-world controllers, real-world models and real-world time conditions. The complex semantics of the given control models and programs is tackled by the use of PLC-timed automata as an easy base model. These automata feature the attributes of the control models as well as the control program. This avoids the explicit construction of intermediate states otherwise necessary. Therefore the number of model states and thus the total complexity of the Translation Validation does not increase which allows the Translation Validation of real-world model sizes.