guest ::
Model-based reliability analysis of aerospace systems
2018 & 2019
Dissertation, RWTH Aachen University, 2018
Veröffentlicht auf dem Publikationsserver der RWTH Aachen University 2019
Genehmigende Fakultät
Fak01
Hauptberichter/Gutachter
;
Tag der mündlichen Prüfung/Habilitation
2018-09-27
Online
DOI: 10.18154/RWTH-2019-02321
URL: https://publications.rwth-aachen.de/record/756236/files/756236.pdf
Einrichtungen
- Lehrstuhl für Informatik 2 (Softwaremodellierung und Verifikation) (121310)
- Fachgruppe Informatik (120000)
Inhaltliche Beschreibung (Schlagwörter)
compass (frei) ; model checking (frei) ; reliability (frei)
Thematische Einordnung (Klassifikation)
DDC: 004
Kurzfassung
Zur Sicherstellung von zuverlässigen und sicheren Systemen, trotz steigender Komplexität und hoher Nachfrage nach Leistungsfähigkeit, werden neuartige Ansätze zur modellbasierten System- und Anwendungsentwicklung im Bereich der Luft und Raumfahrt erarbeitet. Einer dieser Ansätze ist COMPASS. COMPASS bietet einen integrativen Ansatz zur Analyse von Korrektheit, Sicherheit und Leistungsfähigkeit im Luft- und Raumfahrtbereich und stellt eine Vielzahl von Funktionen mit Hilfe einer einzelnen Spezifikationssprache zur Verfügung. Die vorliegende Arbeit beginnt mit einer Beschreibung der verwendeten Modellierungssprache. Die Sprache SLIM, welche sich aus der Sprache AADL ableitet, erlaubt die Spezifikation und Integration von Nominal- und Fehlermodellen. Verschiedenste Abwandlungen werden im Detail erläutert. Im Anschluss hieran wird die Anforderungsspezifikation behandelt, wobei besonderes Augenmerk auf formale Darstellungen gelegt wird. Eine Taxonomie wird definiert, welche es erlaubt unterschiedliche Arten von Anforderungen zu klassifizieren. Anschließend werden verschiedene Ansätze zur Formalisierung von Anforderungen, speziell musterbasierte und auf Entwurfseigenschaften basierende, entwickelt. Letztere führen, zusammen mit der Taxonomie, zur Definition der CSSP, welche Anforderungsspezifikationen direkt im Systemmodell kodiert. Diesem folgt eine Beschreibung der Techniken zur statistischen Modellüberprüfung, welche es erlauben statisch—durch Simulation—das Ergebnis der Modellüberprüfung festzustellen. Im Kontext von COMPASS auftretende, semantische Probleme werden klassifiziert und Lösungswege aufgezeigt. Basierend hierauf wird ein Programm vorgestellt, welches dieses Wissen ausnutzt und von einer probabilistischen Einheit in COMPASS verwendet wird. Neben einer Vielzahl von Verbesserungen in COMPASS wurden auch seine Möglichkeiten und Architektur überholt. Zum Zeitpunkt dieser Arbeit stellt Version 3.0 den aktuellen Stand dar. Erweiterungen hierin beinhalten die Unterstützung von „Timed Failure Propagation Graphs“, nicht-deterministischen Modellen in probabilistischen Analysen, „Contract-Based Analysis“, sowie die neu entwickelte statistische Modellüberprüfung und Ansätze zur Formalisierung von Anforderungen. Schlussendlich wurden sowohl ein Demonstrator als eine Fallstudie erstellt, um COMPASS zugänglicher zu machen. Der Demonstrator verwendet hierbei eine auf SLIM basierende Spezifikation eines Satellitenmodells. Um dies zu erleichtern wird hierfür eine Übersetzung eines Simulink-Modells benutzt. Die vorgestellte Fallstudie basiert auf einer im Rahmen des Projekts durchgeführten Fallstudie und beschreibt Teile der Softwarearchitektur.In order to provide reliable and safe systems in the aerospace domain, despite increased complexity and stronger demands on capabilities, new model-based system and software engineering approaches are being developed. One of which is COMPASS. COMPASS offers an integrated approach to the analysis of correctness, safety and performability of (aerospace) systems, providing a multitude of functions using a single input specification language. This thesis starts with describing the modeling language that is employed by the COMPASS toolset, both its syntax and semantics. Named SLIM, and derived from the AADL, it allows for the specification of nominal and error models, as well as their integration. Various modifications have been made since its first release, which are discussed in-depth. The specification of requirements is treated next, in particular using formal representations. A taxonomy is defined that allows requirements to be classified. Subsequently, different approaches to formalizing requirements are treated, in particular pattern-based and design-attribute based approaches. The latter, combined with the taxonomy, leads to the definition of the catalogue of system and software properties, which encodes requirement specifications directly in the system model. This is followed by a description of statistical model checking techniques. Such techniques allow for statistically determining, by means of simulation, outcomes for the model checking problem. In the setting of COMPASS, semantic issues may arise, which are classified and addressed. A tool making use of this knowledge is described, which is used as a probabilistic engine in the COMPASS toolset. As over the past years the COMPASS toolset has seen numerous enhancements, leading to its latest release—version 3.0. Therefore, its capabilities and architecture are revisited as well. New additions include the support for timed failure propagation graphs, on-deterministic models in probabilistic analysis, contract-based analysis, and the newly developed statistical model checking and requirement formalization approaches. Finally, to make the toolset more accessible, both a demonstrator and a case study have been constructed. The demonstrator deploys a SLIM-based specification on a LEGO® satellite model, making use of a Simulink translator to facilitate this. The case study is based on one performed for the CubETH project, describing part of its software architecture.
OpenAccess: 
PDF
(additional files)
Dokumenttyp
Dissertation / PhD Thesis
Format
online
Sprache
English
Externe Identnummern
HBZ: HT019995615
Interne Identnummern
RWTH-2019-02321
Datensatz-ID: 756236
Beteiligte Länder
Germany
|
The record appears in these collections: |