1995 | OriginalPaper | Chapter
Formale Verifikation der Grundelemente in Funktionsplänen von Notabschaltsystemen
Authors : Wolfgang A. Halang, Bernd Krämer, Norbert Völker
Published in: Verläßliche IT-Systeme
Publisher: Vieweg+Teubner Verlag
Included in: Professional Book Archive
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.