We present a graphical toolset for verifying AADL models, which are gaining widespread acceptance in aerospace, automobile and avionics industries for comprehensively specifying safety-critical systems by capturing functional, probabilistic and hybrid aspects. Analyses are implemented on top of mature model checking tools and range from requirements validation to functional verification, safety assessment via automatic derivation of FMEA tables and dynamic fault trees, to performability evaluation, and diagnosability analysis. The toolset is currently being applied to several case studies by a major industrial developer of aerospace systems.
A Model Checker for AADL / Bozzano, Marco; Cimatti, Alessandro; Katoen, Joost-Pieter; Yen Nguyen, Viet; Noll, Thomas; Roveri, Marco; Wimmer, Ralf. - 6174:(2010), pp. 562-565. (Intervento presentato al convegno CAV 2010 tenutosi a Edinburgh, UK nel 15-19/07/2010) [10.1007/978-3-642-14295-6_48].
A Model Checker for AADL
Alessandro Cimatti;Marco Roveri;
2010-01-01
Abstract
We present a graphical toolset for verifying AADL models, which are gaining widespread acceptance in aerospace, automobile and avionics industries for comprehensively specifying safety-critical systems by capturing functional, probabilistic and hybrid aspects. Analyses are implemented on top of mature model checking tools and range from requirements validation to functional verification, safety assessment via automatic derivation of FMEA tables and dynamic fault trees, to performability evaluation, and diagnosability analysis. The toolset is currently being applied to several case studies by a major industrial developer of aerospace systems.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione
