Formale Analyse von sequential function Charts

Im Rahmen des in zunehmendem Maße geforderten Nachweises der Korrektheit von Steuerungssoftware verfahrenstechnischer, insbesondere pharmazeutischer Anlagen erlangen die Spezifikation der Steuerungen mit geeigneten Sprachen und ihre Analyse in Hinblick auf ihre Korrektheit immer größere Bedeutung. In der Praxis geschieht der Steuerungsentwurf in der Regel aber noch informell ohne den Einsatz geeigneter Spezifikationssprachen oder Dokumentation. Die Überprüfung der Korrektheit erfolgt nicht vollständig, sondern nur durch Tests, die meist erst während der Inbetriebnahme stattfinden, so dass gefundene Fehler u. U. nur noch durch hohen Aufwand zu beheben sind. Ziel dieser Arbeit ist es, einen Beitrag zu einem systematischeren Steuerungsentwurf zu leisten. Dazu wird untersucht, wie sich die Methode der formalen Verifikation für die Analyse von Ablaufsteuerungen einsetzen lässt, die in der Sprache Sequential Function Charts (SFC) programmiert sind. Mit Hilfe der Verifikation ist im Gegensatz zum Test ein formaler Nachweis möglich, dass ein gesteuertes System bestimmte Anforderungen erfüllt. SFC hat als eine graphische Programmiersprache für Speicherprogrammierbare Steuerungen (SPSen) gegenüber den anderen eher implementierungsnahen SPS-Programmiersprachen den Vorteil, dass sie eine prozessnahe, d. h. problemorientierte Sprache ist, die bereits während der Spezifikation und damit durchgängig im Entwurfsprozess eingesetzt werden kann.