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).

Spacecraft Early Design Validation using Formal Methods / Bozzano, M.; Cimatti, A.; Katoen, J. -P.; Katsaros, P.; Mokos, K.; Nguyen, V. Y.; Noll, T.; Postma, B.; Roveri, M.. - In: RELIABILITY ENGINEERING & SYSTEM SAFETY. - ISSN 0951-8320. - STAMPA. - 132:(2014), pp. 20-35. [10.1016/j.ress.2014.07.003]

Spacecraft Early Design Validation using Formal Methods

Cimatti A.;Roveri M.
2014-01-01

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).
2014
Bozzano, M.; Cimatti, A.; Katoen, J. -P.; Katsaros, P.; Mokos, K.; Nguyen, V. Y.; Noll, T.; Postma, B.; Roveri, M.
Spacecraft Early Design Validation using Formal Methods / Bozzano, M.; Cimatti, A.; Katoen, J. -P.; Katsaros, P.; Mokos, K.; Nguyen, V. Y.; Noll, T.; Postma, B.; Roveri, M.. - In: RELIABILITY ENGINEERING & SYSTEM SAFETY. - ISSN 0951-8320. - STAMPA. - 132:(2014), pp. 20-35. [10.1016/j.ress.2014.07.003]
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/258822
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 58
  • ???jsp.display-item.citation.isi??? 47
  • OpenAlex ND
social impact