Bachelor Thesis BCLR-2016-13

BibliographyBalzer, Lukas: Entwicklung eines STPA-Verifiers als Eclipse-Plug-in für die Verifikation von Software-Sicherheitsanforderungen.
University of Stuttgart, Faculty of Computer Science, Electrical Engineering, and Information Technology, Bachelor Thesis No. 13 (2016).
64 pages, german.
CR-SchemaD.2.4 (Software Engineering Software/Program Verification)
I.6.4 (Model Validation and Analysis)
F.1.1 (Models of Computation)
F.4.1 (Mathematical Logic)
Abstract

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.

Full text and
other links
PDF (3065425 Bytes)
Department(s)University of Stuttgart, Institute of Software Technology, Software Engineering
Superviser(s)Wagner, Prof. Stefan; Abdulkhaleq, Asim
Entry dateSeptember 26, 2018
   Publ. Computer Science