Fraunhofer-Gesellschaft

Publica

Hier finden Sie wissenschaftliche Publikationen aus den Fraunhofer-Instituten.

Formal validation methods in model-based spacecraft systems engineering

 
: Katoen, Joost-Pieter; Nguyen, Viet Yen; Noll, Thomas

Gianni, Daniele (Ed.):
Modeling and Simulation-Based Systems Engineering Handbook
Boca Raton, Fla.: CRC Press, 2015 (Engineering Management)
ISBN: 978-1-4665-7145-7
ISBN: 978-1-4665-7146-4
pp.339-376
English
Book Article
Fraunhofer IESE ()
model checking; formal analysis; formal method; formal description technique; safety analysis; performance analysis; correctness; satellite control

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. That is why we developed - with 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 the Architecture Analysis and Design Language (AADL) and enables engineers to express the spacecraft system design, the software design, and their reliability aspects in a single integrated model. The model can subsequently be analyzed by the COMPASS toolset. This toolset utilizes state-of-the-art model checking techniques, both qualitative and probabilistic, for checking requirements related to functional correctness, safety & dependability and performance. Several studies using satellite design data have been performed by industry. We report on them in this chapter. The formal nature of our approach enables engineers to identify, evaluate and address intricate strengths and weaknesses in the system software architecture through rigorous and automated methods. Our experience report on these methods with our satellite cases can be used to kickstart future formal model-based validation efforts.

: http://publica.fraunhofer.de/documents/N-323536.html