Model-based reliability analysis of aerospace systems

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