Abstract
| Original language | Undefined |
|---|---|
| Pages (from-to) | 20-35 |
| Number of pages | 16 |
| Journal | Reliability engineering & system safety |
| Volume | 132 |
| DOIs | |
| Publication status | Published - Dec 2014 |
Keywords
- EWI-25692
- IR-94429
- METIS-309876
Cite this
}
Spacecraft early design validation using formal methods. / Bozzano, Marco; Cimatti, Alessandro; Katoen, Joost P.; Katsaros, Panagiotis; Mokos, Konstantinos; Nguyen, Viet Yen; Noll, Thomas; Postma, Bart; Roveri, Marco.
In: Reliability engineering & system safety, Vol. 132, 12.2014, p. 20-35.Research output: Contribution to journal › Article › Academic › peer-review
TY - JOUR
T1 - Spacecraft early design validation using formal methods
AU - Bozzano, Marco
AU - Cimatti, Alessandro
AU - Katoen, Joost P.
AU - Katsaros, Panagiotis
AU - Mokos, Konstantinos
AU - Nguyen, Viet Yen
AU - Noll, Thomas
AU - Postma, Bart
AU - Roveri, Marco
N1 - eemcs-eprint-25692
PY - 2014/12
Y1 - 2014/12
N2 - 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).
AB - 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).
KW - EWI-25692
KW - IR-94429
KW - METIS-309876
U2 - 10.1016/j.ress.2014.07.003
DO - 10.1016/j.ress.2014.07.003
M3 - Article
VL - 132
SP - 20
EP - 35
JO - Reliability engineering & system safety
JF - Reliability engineering & system safety
SN - 0951-8320
ER -