Programmanalyse und Verifikation von SPS-Programmen

Autor: Kucera, Gernot
Jazyk: němčina
Rok vydání: 2017
Předmět:
DOI: 10.34726/hss.2017.50347
Popis: 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.
Databáze: OpenAIRE
Externí odkaz: