Title
Spacecraft early design validation using formal methods.
Abstract
The size and complexity of software in spacecraft is increasing exponentially, and this trend complicates its validation within the context of the overall spacecraft system. Current validation methods are labor-intensive as they rely on manual analysis, review and inspection. For future space missions, we developed – with challenging requirements from the European space industry – a novel modeling language and toolset for a (semi-)automated validation approach. Our modeling language is a dialect of AADL and enables engineers to express the system, the software, and their reliability aspects. The COMPASS toolset utilizes state-of-the-art model checking techniques, both qualitative and probabilistic, for the analysis of requirements related to functional correctness, safety, dependability and performance. Several pilot projects have been performed by industry, with two of them having focused on the system-level of a satellite platform in development. Our efforts resulted in a significant advancement of validating spacecraft designs from several perspectives, using a single integrated system model. The associated technology readiness level increased from level 1 (basic concepts and ideas) to early level 4 (laboratory-tested).
Year
DOI
Venue
2014
10.1016/j.ress.2014.07.003
Reliability Engineering & System Safety
Keywords
DocType
Volume
Safety and dependability analysis,Performance analysis,Model checking,AADL modeling language,Spacecraft
Journal
132
ISSN
Citations 
PageRank 
0951-8320
2
0.42
References 
Authors
0
9
Name
Order
Citations
PageRank
Marco Bozzano174349.82
Alessandro Cimatti25064323.15
Joost-Pieter Katoen34444289.65
Panagiotis Katsaros420.42
Konstantinos Mokos520.42
Viet Yen Nguyen623213.38
Thomas Noll732627.79
Bart Postma8141.14
Marco Roveri9171.47