Formale Verifikation der Grundelemente in Funktionsplänen von Notabschaltsystemen

Die Aufgabe von Schutzsystemen besteht darin, Prozesse aus gefährlichen in sichere Zustände zu bringen. Eine besondere Klasse von Schutzsystemen sind Notabschaltsysteme (NAS), die bis jetzt nur in inhärent fehlersicherer, festverdrahteter Form realisiert werden. Trotz ihrer hohen Zuverlässigkeit gibt es in der Industrie einen dringenden Bedarf, sie durch flexiblere Systeme zu ersetzen. Daher wird eine besondere speicherprogrammierbare Steuerung (SPS) vorgestellt, die Funktionspläne (FUP), das traditionelle und anwenderorientierte Paradigma für NASe, in ihrer Architektur direkt unterstützt. Dann geben wir einen formalen Korrektheitsbeweis der in FU-Pen auftretenden und NASe spezifizierende funktionalen Elemente. Bei dieser Aufgabe wird Isabelle/HOL als mechanischer Beweisassistent eingesetzt. Als letzter Schritt kann die Sicherheitsabnahme von NAS-Software leicht durch eine Rückübersetzung durchgeführt werden, eine besonders einfache, aber rigorose Methode, die auch von der SPS-Architektur unterstützt wird.