We report on a model-based approach to system-software co-engineering which is tailored to the specific characteristics of critical on-board systems for the aerospace domain. The approach is supported by a System-Level Integrated Modeling (SLIM) Language by which engineers are provided with convenient ways to describe nominal hardware and software operation, (probabilistic) faults and their propagation, error recovery, and degraded modes of operation. Correctness properties, safety guarantees, and performance and dependability requirements are given using property patterns which act as parameterized "templates" to the engineers and thus offer a comprehensible and easy-to-use framework for requirement specification. Instantiated properties are checked on the SLIM specification using state-of-the-art formal analysis techniques such as bounded SAT-based and symbolic model checking, and probabilistic variants thereof. The precise nature of these techniques together with the formal SLIM sem...
The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems / Bozzano, Marco; Cimatti, Alessandro; Katoen, Joost-Pieter; Yen Nguyen, Viet; Noll, Thomas; Roveri, Marco. - 5775:(2009), pp. 173-186. ( 28th International Conference on Computer Safety, Reliability, and Security, SAFECOMP 2009 Hamburg, Germany 15-18/09/2009) [10.1007/978-3-642-04468-7_15].
The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems
Alessandro Cimatti;Marco Roveri
2009-01-01
Abstract
We report on a model-based approach to system-software co-engineering which is tailored to the specific characteristics of critical on-board systems for the aerospace domain. The approach is supported by a System-Level Integrated Modeling (SLIM) Language by which engineers are provided with convenient ways to describe nominal hardware and software operation, (probabilistic) faults and their propagation, error recovery, and degraded modes of operation. Correctness properties, safety guarantees, and performance and dependability requirements are given using property patterns which act as parameterized "templates" to the engineers and thus offer a comprehensible and easy-to-use framework for requirement specification. Instantiated properties are checked on the SLIM specification using state-of-the-art formal analysis techniques such as bounded SAT-based and symbolic model checking, and probabilistic variants thereof. The precise nature of these techniques together with the formal SLIM sem...I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione
