UML-basierte Modellierung und Verifikation von Steuerungen

Die Komplexität von Steuerungen und deren Anwendungen in sicherheitskritischen Bereichen der Automatisierungstechnik erfordern ein hohes Maß an Betriebssicherheit. Mit zunehmender Komplexität der Systeme steigt der Bedarf, Systemkonzepte vorab durch simulationsbasierte und formale Verifikationsverfahren hinsichtlich geforderter Eigenschaften zu bewerten. Grundlage dafür ist ein gemeinsames Modell von Steuerung und Anlage, wobei die Steuerung durch UML-konforme Zustandsdiagramme und die Analge durch ein Blockmodell in Modelica-Codierung beschrieben wird. Als Verifikationsverfahren werden Design Rule Checking, Assertion Based Verification und Model Checking eingesetzt. Im Design Rule Checking werden Struktureigenschaften des UML-Zustandsdiagramms der Steuerung überprüft. Erkannte Fehler sind z. B. isolierte Teilgraphen und nicht eindeutige Schalt-Prioritäten von Transitionen. Die Assertion Based Verification ist ein Verifikationszugang, der auf die Überwachung temporaler Systemeigenschaften während der Simulation zielt. Diese Eigenschaften werden in Assertion Charts formuliert. Assertion Charts haben die Struktur von UML-Zustandsdiagrammen und werden wie die Steuerung und das physikalische Anlagenmodell in Modelica-Code übersetzt. Die Assertion Charts werden parallel zum Modell des Automatisierungssystems ausgeführt - sie fungieren als Beobachter des Systems zur Simulationszeit. Das Model Checking ist ein automatisches Verfahren zum Beweis von Systemeigenschaften. Das UML-Zustandsdiagramm der Steuerung wird dazu in die Eingabesprache des Model Checker NuSMV übersetzt. Die Reaktionen der Anlage werden zeitlich diskretisiert in Tabellenmodellen in den Modellvorrat integriert. Als weitere Eingabe erhält der Model Checker die Beschreibung der geforderten Eigenschaften in temporal-logischen Ausdrücken. Die Ausführung des Checks liefert die Aussage, ob die Eigenschaften erfüllt sind oder nicht. Im negativen Fall enthält die Ausgabe ein Gegenbeispiel. Die Assertion Based Verification und das Model Checking werden am Beispiel einer Verpackungsmaschine demonstriert.