Programmanalyse und Verifikation von SPS-Programmen

Abstract

Speicherprogrammierbare Steuerungen (SPS) werden zur Lösung von Automatisierungsaufgaben technischer Systeme und Anlagen genutzt. Die Herausforderung an die moderne Automatisierungstechnik ist die Beherrschung der Komplexität von Prozessen. Innerhalb dieser Prozesse ist dies durch die steigende Anzahl der Signale und damit verbunden durch immer größere Datenmengen gekennzeichnet. In den dazu verwendeten Rechnersystemen nehmen SPS eine wichtige Rolle ein. Nicht nur Steuerungsaufgaben, sondern auch Betrachtungen zur Zuverlässigkeit und zur Sicherheit und die Umsetzung geeigneter Maßnahmen dazu werden immer stärker in den Mittelpunkt der Automatisierung gerückt. Als programmgesteuerte Automatisierungscomputer werden SPS in nahezu allen Bereichen der Anlagentechnik beginnend bei chemisch technologischen Anlagen bis hin zu Maschinensteuerungen eingesetzt. SPS werden darin als sichere Rechensysteme für hoch verlässliche Steuerung und Regelung technischer Prozesse genutzt. Der ständig steigende Automatisierungsgrad neuer technischer Systeme und der Wunsch nach immer mehr Funktionalität und Flexibilität in Automatisierungseinrichtungen führen zwangsläufig zu höherer Komplexität der sie bereitstellenden Hard- und Softwaresysteme. Damit wird die Frage der Zuverlässigkeit und Sicherheit zum zentralen Problem des Entwurfs und der Realisierung neuartiger Automatisierungssysteme. Nicht nur für in sicherheitsrelevanten Anwendungen eingesetzte SPS Systeme muss für das betrachtete System das ausfallsicherheitsgerichtete Verhalten nachgewiesen werden. Dazu sind oft zeitaufwändige Tests während der Phase der Inbetriebsetzung notwendig. Anlagefunktionen werden dabei verifiziert und validiert. Eine wesentliche Rolle spielen dabei die SPS-Programme. Weil die Leistungsfähigkeit von SPS-Systemen im Zuge der technischen Weiterentwicklung zusammen mit den Anforderungen an solche Systeme Schritt gehalten hat, sind Systeme mit mehreren Tausend Signalzuständen die Regel und nicht die Ausnahme. Das exponentielle Anwachsen der möglichen Systemzustände ist bekannt als das „state explosion problem“, die Beherrschung des Problems Gegenstand der Forschung. Als Beitrag zur Beherrschung der Komplexität zeigt diese Arbeit, wie durch die Zerlegung der Systemfunktionalität eines umfangreichen durch eine SPS gesteuerten Systems die Gesamtaufgabe einer Verifikation automatisiert unterstützt wird, in dem durch Segmentierung SPS-Programmbereiche definiert werden, die im Sinne der Gesamtfunktion von Programmteilen überblickbar und damit handhabbar werden. Diese SPS-Programmbereiche werden einzeln einer Verifikation zugänglich gemacht. Die Zerlegung selbst erfolgt durch automatisierte Analyse des vom Anwender einer SPS erstellten Anwender-Programms. Die Analyse von Anwender-Programmen speicherprogrammierbarer Steuerungen ist ein Teilschritt für die automatisierte Verifikation. Zweck der Analyse ist es, einerseits mögliche Probleme im Programm einer SPS aufzudecken und andererseits ein SPS-Programm einer weitgehend automatisierten Verifikation zugänglich zu machen. In der Folge werden Programmkonstrukte einer SPS als Segmente bezeichnet, die gleichzeitig einzeln verifizierbare Einheiten sind. Frei nach dem Ausspruch „divide et impera“ kann mit Hilfe von Analysetechniken ein SPS-Programm geeignet zerlegt werden. Bezogen auf einzelne Segmente wird dadurch der Untersuchungsraum stark verkleinert. Die zulässige Größe eines Segments kann durch das Verändern seiner Grenzen an die Rechenleistung des Untersuchungssystems angepasst werden. Einzige Voraussetzung für die Verifikation ist, dass ein SPS-Programm vollständig untersucht wird. Deshalb werden bei Mehrfachverwendung von Informationen die Segmentgrenzen im Untersuchungsraum derart angepasst, dass auch Überschneidungen durch Mehrfachverwendung von Programmelementen vollständig bei der Bearbeitung berücksichtigt werden. Zweckmäßigerweise werden hierzu Minima für die Überschneidungen bestimmt. Die Tatsache, dass bei einem SPS-Programm von „Linearität“ bei der Programmbearbeitung ausgegangen werden kann, weil speziell bei sicherheitsrelevanten Steuerungen Programmkonstrukte mit Rückwärtssprüngen oder Programmschleifen unzulässig sind, erleichtert die Aufgabe. Untersucht wird der vollständige Lösungsraum innerhalb jedes Segments. Genügen daher alle Kombinationen der als Startbedingung vorausgesetzten Eingangsabbilder (Eingangsvektoren) den Anforderungen an die Ausgangsabbilder (Ausgangsvektoren), ist die Verifikation erfolgreich. Durch Rückwärtsanalyse werden für jeden SPS-Ausgang die bestimmenden Elemente zugeordnet. Damit wird der Lösungsraum vollständig in Bezug auf die Ausgangsabbilder abgebildet. Das zugehörige Konzept für die Verifikation folgt den Regeln klassischer Verifikationstechniken: Eingangsabbilder werden als Vorbedingungen behandelt und mathematisch untersucht, ob zugehörige Ausgangsabbilder als Ergebnis erreicht werden. Anstatt den gesamten Verifikationsschritt auf einmal durchzuführen, wird ein mehrfach gestuftes Verfahren vorgeschlagen. Grob gesehen können Schritte identifiziert werden: die Voruntersuchungen zur Syntax mit semantischen Anteilen, die Zerlegung mit Verifikation von Teilbereichen und die Untersuchung auf Vollständigkeit. Das Ende einer Untersuchung, die erfolgreiche Verifikation, ist nicht von der Reihenfolge der Festlegung der Prämissen für die Verifikation abhängig. Im konventionellen Ansatz zur Verifikation werden zuerst die Bedingungen definiert zusammen mit zu erzielenden Ergebnissen, um in Relation mit dem Quellcode in möglichst wenigen Schritten eine Entscheidung herbeizuführen. Prinzipiell ist dies beim hier verfolgten Ansatz genauso. Im Unterschied dazu erlaubt jedoch die hier verfolgte Methode die Nutzung auch so genannter „offener“ Referenzen, die erst in einem weiteren Zwischenschritt zu Prämissen werden. Zuletzt werden Verifikationsergebnisse von Teilbereichen zu einer Verifikation des gesamten SPS-Programms rekombiniert.

Programmable Logic Controllers (PLC) are used in automation of technical systems and machines. The challenge for modern automation is in the handling of the complexity of the processes. These processes are characterized by an increasing number of signals and linked to this is an increasing amount of data. PLC used in the processing systems play an important role. Not only controlling tasks but also reliability and safety issues and their realisation come more and more into the focus of automation. PLC are used as programmable automation controllers in almost all areas of plant engineering all the way from chemical plants to production machinery controls. In these fields PLC are used as safe computing systems for safety relevant controls and feedback control of technical processes. The increasing level of automation in new technical systems and the demand for more and more functionality and flexibility in automation systems inevitably lead towards higher complexity of supporting hardware and software systems. This makes problems of reliability and safety a central problem in design and realisation of new automation systems. Safeguarding against failure for systems in question must be verified not only for safety relevant applications. This often calls for time-consuming testing during installation of systems. System functionalities get verified and validated in the process. PLC software plays a critical role in this. As the performance of PLC systems has increased with modern technical enhancements together with the requirements for such systems, nowadays systems with several thousands of signal conditions are no exceptions any more but rather state of the art. The exponential growth of possible system states is known as “state explosion problem“ and research currently focuses on dealing with this problem. This thesis contributes to handling the complexity by showing how automated verification of a large PLC controlled system can be supported by breaking down the functionality of the system. This is achieved by segmenting PLC program components to make them straightforward and therefore manageable in the sense of the full functionality. These PLC program segments will now be put to verification part by part. The segmentation itself is done by means of automatic analysis of the user-generated PLC program. Analysing user programs for programmable logic controllers (PLC) is a step towards automatic verification. Purpose of the analysis is on one hand to find possible problems in the PLC program and on the other hand to make the PLC program available for an in most parts automated program verification. Subsequently, program constructs for PLC will be called segments, which will at the same time be stand-alone verifiable components. According to the saying “divide et impera“ analysis techniques can be used to fittingly decompose a PLC program. Regarding single segments, the scope for examination will be made significantly smaller by this. The size of one segment can be adapted to the performance capabilities of the analysing system by reducing its size. The only requirement for verification is that the PLC program must be analysed completely. Therefore, if information is used repeatedly, segment borders will be adapted in such a way that overlapping of code parts is fully considered during processing. Overlapping minima will be defined appropriately for this purpose. The task is made easier by the fact that linearity can be assumed with PLC programs as in safety relevant programs loops and backward jumps are not allowed. For each segment the full solution space will be analysed. So if all possible combinations of input images (input vectors) satisfy the requirements of the output images (output vectors) the verification is successful. By backward analysis every PLC output has its determining elements assigned. By this the solution space will be fully mapped with regard to the output images. The associated verification concept for the verification clings to the common verification rules. Input images will be considered as preconditions and mathematically analysed if they lead towards corresponding output images as results. Instead of performing a complete verification in one single step, a multiple step approach is suggested. In a bigger picture, the following steps can be identified: syntactic pre-examinations with semantic parts, breaking the system down and verifying portions, and a test for completeness An examination finish, the successful verification, does not depend on the order of defining the assumptions for verification. In the conventional approach first all conditions together with the expected results are defined to provide a result together with the source code in as little steps as possible. The approach discussed here basically works the same but the method described allows for so called open references which will become assumptions only at later steps. Finally, all verification results for the various parts will be recombined into a verification of the complete PLC program.