Speicherprogrammierbare Steuerungen werden häufig in sicherheitskritischen Systemen
verwendet. Einfaches Testen dieser Systeme reicht häufig nicht aus, da bestimmte Fehler
durch Testen alleine schwer zu finden sind. Model-Checking ist eine formale Methode, die
zeigen kann, dass ein System seine Spezifikation erfüllt. Existierende Ansätze zum Model-
Checking übersetzen dazu die SPS-Programme in die Eingabesprache eines existierenden
Model-Checkers. Diese Arbeit beschreibt einen neuen Ansatz zum Model-Checking von
SPS-Programmen, der direkt auf den SPS-Programmen arbeitet, ohne diese zu übersetzen.
Dadurch kann während der Verifikation auf domänenspezifische Informationen zugegriffen
werden und Gegenbeispiele werden in der Sprache angezeigt in der das SPS-Programm
geschrieben wurde. Dieses erleichtert den Entwicklern die Lokalisierung von Fehlern. Der
beschriebene Ansatz verwendet zum Aufbau der Zustandsräume angepasste Simulatoren,
die automatisch Abstraktionstechniken anwenden, um das Zustandsexplosionsproblem anzugehen.
Einige Fallstudien zeigen die Anwendbarkeit des vorgestellten Ansatzes.