Funktionale Sicherheit nach IEC 61508 umzusetzen und nachzuweisen ist heutzutage eine große Herausforderungen im Design von Automatisierungssystemen. Viele dieser Systeme werden mittels einer Speicherprogrammierbaren Steuerung (SPS) realisiert und nach IEC 61131-3 programmiert. Die PLCopen spezifizierte hierfür eine Bibliothek von Funktionsbausteinen (FB) zur Programmierung sicherheitsgerichteter Anwendungen. Dieser Beitrag präsentiert eine Methodik zur Verifikation und Validierung solcher Anwendungen. Die Programme werden dabei zunächst in ein System zeitbehafteter Automaten überführt und anschließend durch den UPPAAL-Modelchecker formal verifiziert und simulativ validiert. Zur leichteren Anwendung wird zudem ein Ansatz zur automatisierten Übertragung von Simulationsszenarien aus einer Soft-SPS in den Modelchecker UPPAAL vorgeschlagen