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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione