Erweiterung der Einzelplatzanwendung des Systems XSTAMPP 4 um die Verfeinerung des Unsafe Control Actions für ein Model Check

Abstract

System-Theoretic Process Analysis (STPA) ist eine Technik, die zur Gefährdungsanalyse komplexer Systeme eingesetzt werden kann [Lev16]. Das an der Universität Stuttgart entwickelte System NAXT ist ein Programm zur Durchführung von STPA-Analysen. Die Software in Systemen kann Ursprung von Gefährdungen sein, um diese zu verhindern ist die Verifikation der Software sinnvoll. Allerdings unterstützt NAXT bisher die Analyse der in den Systemen eingesetzten Software nicht. Asim Abdulkhaleq und Stefan Wagner stellen in ihren Arbeiten [AW15; AWL15] eine Möglichkeit vor, die Verifikation von Software in den STPA-Prozess einzubauen. Diese Arbeit stellt den Entwurf und die Umsetzung einer Erweiterung von STPA in NAXT um diesen Schritt vor. NAXT wird das Verifizieren von Software durch Model Checking erleichtern. Hierfür wird eine Möglichkeit geboten, Anforderungen an die Software abzuleiten und formal zu erfassen. Ebenfalls wird eine Möglichkeit geboten, eine Verifikation mit den Programmen NuSMV und SPIN aus NAXT zu starten.