Spacecraft early design validation using formal methods

Marco Bozzano, Alessandro Cimatti, Joost P. Katoen, Panagiotis Katsaros, Konstantinos Mokos, Viet Yen Nguyen, Thomas Noll, Bart Postma, Marco Roveri

Research output: Contribution to journal › Article

  • 17 Citations

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).
LanguageUndefined
Pages20-35
Number of pages16
JournalReliability engineering & system safety
Volume132
DOIs
StatePublished - Dec 2014

Keywords

  • EWI-25692
  • IR-94429
  • METIS-309876

Cite this

Bozzano, M., Cimatti, A., Katoen, J. P., Katsaros, P., Mokos, K., Nguyen, V. Y., ... Roveri, M. (2014). Spacecraft early design validation using formal methods. Reliability engineering & system safety, 132, 20-35. DOI: 10.1016/j.ress.2014.07.003
Bozzano, Marco ; Cimatti, Alessandro ; Katoen, Joost P. ; Katsaros, Panagiotis ; Mokos, Konstantinos ; Nguyen, Viet Yen ; Noll, Thomas ; Postma, Bart ; Roveri, Marco. / Spacecraft early design validation using formal methods. In: Reliability engineering & system safety. 2014 ; Vol. 132. pp. 20-35
@article{70f1048cd0fa4a86894923146e64f494,
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).",
keywords = "EWI-25692, IR-94429, METIS-309876",
author = "Marco Bozzano and Alessandro Cimatti and Katoen, {Joost P.} and Panagiotis Katsaros and Konstantinos Mokos and Nguyen, {Viet Yen} and Thomas Noll and Bart Postma and Marco Roveri",
note = "eemcs-eprint-25692",
year = "2014",
month = "12",
doi = "10.1016/j.ress.2014.07.003",
language = "Undefined",
volume = "132",
pages = "20--35",
journal = "Reliability engineering & system safety",
issn = "0951-8320",
publisher = "Elsevier Limited",

}

Bozzano, M, Cimatti, A, Katoen, JP, Katsaros, P, Mokos, K, Nguyen, VY, Noll, T, Postma, B & Roveri, M 2014, 'Spacecraft early design validation using formal methods' Reliability engineering & system safety, vol 132, pp. 20-35. DOI: 10.1016/j.ress.2014.07.003

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

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

T2 - Reliability engineering & system safety

JF - Reliability engineering & system safety

SN - 0951-8320

ER -

Bozzano M, Cimatti A, Katoen JP, Katsaros P, Mokos K, Nguyen VY et al. Spacecraft early design validation using formal methods. Reliability engineering & system safety. 2014 Dec;132:20-35. Available from, DOI: 10.1016/j.ress.2014.07.003

Access to Document