This paper reports on a model-based approach to system-software co-engineering which is tailored to critical on-board systems for the aerospace domain but is relevant to a much wider class of dependable systems. Our main contribution is a formal semantics for a greater part of standardised AADL, the Architecture Analysis and Design Language, and its Error Model Annex. It covers nominal and degraded hardware/software operations, hybrid (and timing) aspects as well as probabilistic faults, their propagation and recovery. The accompanying software toolset employs SAT-based and symbolic model checking techniques and probabilistic variants thereof. The precise nature of these techniques together with the formal semantics provide a trustworthy modelling and analysis framework to support, among others, assessment of functional correctness, evaluation of performance measures and automated derivation of dynamic fault trees, FMEA tables and observability requirements.

Verification and performance evaluation of AADL models / Bozzano, Marco; Cimatti, Alessandro; Roveri, Marco; Katoen, Joost-Pieter; Yen Nguyen, Viet; Noll, Thomas. - (2009), pp. 285-286. (Intervento presentato al convegno ESEC/FSE 2009 tenutosi a Amsterdam, The Netherlands nel 24-28/08/2009) [10.1145/1595696.1595744].

Verification and performance evaluation of AADL models

Alessandro Cimatti;Marco Roveri;
2009-01-01

Abstract

This paper reports on a model-based approach to system-software co-engineering which is tailored to critical on-board systems for the aerospace domain but is relevant to a much wider class of dependable systems. Our main contribution is a formal semantics for a greater part of standardised AADL, the Architecture Analysis and Design Language, and its Error Model Annex. It covers nominal and degraded hardware/software operations, hybrid (and timing) aspects as well as probabilistic faults, their propagation and recovery. The accompanying software toolset employs SAT-based and symbolic model checking techniques and probabilistic variants thereof. The precise nature of these techniques together with the formal semantics provide a trustworthy modelling and analysis framework to support, among others, assessment of functional correctness, evaluation of performance measures and automated derivation of dynamic fault trees, FMEA tables and observability requirements.
2009
Proceedings of the the 7th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering
USA
ACM
9781605580012
Bozzano, Marco; Cimatti, Alessandro; Roveri, Marco; Katoen, Joost-Pieter; Yen Nguyen, Viet; Noll, Thomas
Verification and performance evaluation of AADL models / Bozzano, Marco; Cimatti, Alessandro; Roveri, Marco; Katoen, Joost-Pieter; Yen Nguyen, Viet; Noll, Thomas. - (2009), pp. 285-286. (Intervento presentato al convegno ESEC/FSE 2009 tenutosi a Amsterdam, The Netherlands nel 24-28/08/2009) [10.1145/1595696.1595744].
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/258708
 Attenzione

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

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