The size and complexity of control software in aerospace systems is rapidly increasing, and this development complicates its validation within the con- text of the overall spacecraft system. Classical validation methods are both labour intensive and error prone as they rely on manual analysis, review and inspection. Thus there is a growing trend to incorporate the use of automated formal methods. This chapter introduces the ESA-funded COMPASS project, which aims at an integrated system-software co-engineering approach focusing on a coherent set of specification and analysis techniques for evaluation of system-level correctness, safety, dependability and performability of on-board computer-based aerospace sys- tems. Its modelling features and supporting toolset provide a unifying framework for system validation, employing state-of-the-art temporal-logic model checking tech- niques for infinite-state transition systems, both qualitative and probabilistic, with extensions to fault detection, identification and recovery (FDIR) and safety analysis. We provide an overview of the technology and of the results that have been achieved so far, and address several challenges for future developments. Current efforts of the project consortium concentrate on improving and advancing both process as well as technology of the COMPASS approach, with the goal of bringing the methods to higher levels of technology readiness

Formal Methods for Aerospace Systems

Marco Bozzano;Alessandro Cimatti;Stefano Tonetta
2017-01-01

Abstract

The size and complexity of control software in aerospace systems is rapidly increasing, and this development complicates its validation within the con- text of the overall spacecraft system. Classical validation methods are both labour intensive and error prone as they rely on manual analysis, review and inspection. Thus there is a growing trend to incorporate the use of automated formal methods. This chapter introduces the ESA-funded COMPASS project, which aims at an integrated system-software co-engineering approach focusing on a coherent set of specification and analysis techniques for evaluation of system-level correctness, safety, dependability and performability of on-board computer-based aerospace sys- tems. Its modelling features and supporting toolset provide a unifying framework for system validation, employing state-of-the-art temporal-logic model checking tech- niques for infinite-state transition systems, both qualitative and probabilistic, with extensions to fault detection, identification and recovery (FDIR) and safety analysis. We provide an overview of the technology and of the results that have been achieved so far, and address several challenges for future developments. Current efforts of the project consortium concentrate on improving and advancing both process as well as technology of the COMPASS approach, with the goal of bringing the methods to higher levels of technology readiness
2017
978-981-10-4435-9
File in questo prodotto:
File Dimensione Formato  
main.pdf

solo utenti autorizzati

Tipologia: Documento in Pre-print
Licenza: NON PUBBLICO - Accesso privato/ristretto
Dimensione 1.6 MB
Formato Adobe PDF
1.6 MB Adobe PDF   Visualizza/Apri   Richiedi una copia

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/11582/316118
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact