Erweiterung von MBSE Prozessen bei der Entwicklung sicherheitskritischer Systemarchitekturen durch die Nutzung Formaler Methoden

Kurzfassung

Die Komplexität von sicherheitskritischen Systemen ist seit jeher gewachsen, aber besonders in den letzten zwei Jahrzehnten mit dem Anstieg von Komponenten, Funktionen und Interaktionen. Traditionelle Entwicklungsprozesse stehen dementsprechend vor großen Herausforderungen. Sie müssen die Sicherheit der Systeme unter steigender Komplexität und Zeitdruck garantieren. In dieser Masterarbeit wird ein Prozess vorgestellt, der sich dieser Herausforderung annimmt, indem auf Model Based System Engineering (MBSE), System Theoretic Process Analysis (STPA) und Formale Methoden zurückgegriffen wird. Als Grundlage für den vorgeschlagenen Entwicklungsprozess wird MBSE verwendet, welches als multi-disziplinärer und integrativer Prozess zur systematischen Entwicklung von Systemen beschrieben werden kann. Luftfahrt- und Automobilsysteme sind sicherheitskritisch und auf ausführliche Sicherheitsbetrachtungen angewiesen, um eine Zulassung zu bekommen. Während Sicherheitsanalysen traditionell von einem unterschiedlichen Team von Sicherheitsingenieuren anhand von Dokumenten ausgeführt werden, schlägt diese Arbeit eine, mit Formalen Methoden gestützte, Integration der STPA-Sicherheitsanalyse in den MBSE-Prozess vor. Die STPA stellt eine vielversprechende Sicherheitsanalyse dar, die genau wie das MBSE auf der System-Theorie beruht und dementsprechend gut in eine MBSE-Entwicklung integriert werden kann. Durch die Formalisierung der STPA können einige manuelle Schritte der Sicherheitsanalyse automatisiert werden. Die Systems Modeling Language (SysML), die als Grundlage für die MBSE-Modelle genutzt wird, stellt durch ihre semi-formalen Eigenschaften einen geeigneten Kandidaten für die Formalisierung dar. Außerhalb der Durchführung der STPA können auch die entstehenden Sicherheitsanforderungen zum Teil formalisiert und überprüft werden. Für eine formale Überprüfung statischer Sicherheitsanforderungen empfiehlt diese Arbeit die Nutzung der Object Constraint Language (OCL), die standardisiert in Kombination mit der SysML genutzt werden kann. Für die Überprüfung von dynamischen Sicherheitsanforderungen wird die Nutzung von formalen Sprachen basierend auf temporalen Logiken vorgeschlagen, die eine formale Argumentation über zeitliche Eigenschaften ermöglichen. Zusammengefasst stellt diese Arbeit einen ganzheitlichen Prozess vor, der Sicherheitsbetrachtungen mit Formalen Methoden in eine MBSE-Entwicklung integriert und damit ermöglicht, den Komplexitätsanstieg von Systemen zu managen.