756236 20251028101824.0 HBZ HT019995615 Laufende Nummer 38074 datacite_doi 10.18154/RWTH-2019-02321 RWTH-2019-02321 English 004 P:(DE-82)IDM01581 Bruintjes, Harold Yorick 0 rwth Model-based reliability analysis of aerospace systems vorgelegt von Harold Y. Bruintjes, Master of Science online Aachen 2018 2019 1 Online-Ressource (xii, 244 Seiten) : Illustrationen, Diagramme 2 EndNote Thesis PUB:(DE-HGF)11 PUB:(DE-HGF) Dissertation / PhD Thesis phd phd BibTeX PHDTHESIS DRIVER doctoralThesis DataCite Output Types/Dissertation ORCID DISSERTATION Veröffentlicht auf dem Publikationsserver der RWTH Aachen University 2019 Dissertation, RWTH Aachen University, 2018 Dissertation RWTH Aachen University 2018 Fak01 2018-09-27 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. ger 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. eng Dataset connected to Lobid/HBZ Germany compass model checking reliability P:(DE-82)IDM00048 Katoen, Joost-Pieter 1 Thesis advisor rwth P:(DE-82)023342 Cimatti, Alessandro 2 Thesis advisor http://publications.rwth-aachen.de/record/756236/files/756236.pdf OpenAccess http://publications.rwth-aachen.de/record/756236/files/756236_source.zip Restricted http://publications.rwth-aachen.de/record/756236/files/756236.gif?subformat=icon icon OpenAccess http://publications.rwth-aachen.de/record/756236/files/756236.jpg?subformat=icon-1440 icon-1440 OpenAccess http://publications.rwth-aachen.de/record/756236/files/756236.jpg?subformat=icon-180 icon-180 OpenAccess http://publications.rwth-aachen.de/record/756236/files/756236.jpg?subformat=icon-640 icon-640 OpenAccess http://publications.rwth-aachen.de/record/756236/files/756236.jpg?subformat=icon-700 icon-700 OpenAccess oai:publications.rwth-aachen.de:756236 openaire open_access VDB driver dnbdelivery I:(DE-588b)36225-6 P:(DE-82)IDM01581 RWTH Aachen 0 RWTH I:(DE-588b)36225-6 P:(DE-82)IDM00048 RWTH Aachen 1 RWTH 2018 StatID:(DE-HGF)0510 StatID OpenAccess I:(DE-82)121310_20140620 121310 Lehrstuhl für Informatik 2 (Softwaremodellierung und Verifikation) 0 I:(DE-82)120000_20140620 120000 Fachgruppe Informatik 1 FullTexts I:(DE-82)120000_20140620 I:(DE-82)121310_20140620 UNRESTRICTED VDB phd