Um die Sicherheit in kritischen Softwaresystemen zu gewährleisten ist immer häufiger eine Verifikation der Software in einem Systemkontext notwendig. Hierfür ist in den letzten Jahren die Verifikation von Softwaresystemen durch Model Checking, bedingt durch die wachsende Anzahl an dafür zur Verfügung stehenden Werkzeugen, eine bewährte Methode geworden. Diese Arbeit stellt auf Grundlage des in STPA SwISS [AWL15] vorgestellten Konzeptes eine Software zur automatisierten Ausführung von LTL und CTL Model Checking mit den Werkzeugen Spin und NuSMV bietet. Dabei können die Sicherheitsanforderungen sowohl manuell eingegeben werden, als auch aus einer STPA Analyse importiert werden. Das Ergebnis dieser Arbeit soll ein Ansatz zur Kombination einer Gefahrenanalyse auf Systemebene und einer Verifikation dieses Systems auf Implementierungsebene sein. Zu diesem Zweck wird der STPA Verifier zur automatisierten Verifikation von Sicherheitsanforderungen und Dokumentation der Ergebnisse vorgestellt.
