Verification and performance evaluation of aadl models

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.

REFERENCES

• 1: Website of the COMPASS Project: http://compass.informatik.rwth-aachen.de/
• 2: M. Bozzano, A. Cimatti, M. Roveri, J.-P. Katoen, V. Y. Nguyen, T. Noll, Codesign of Dependable Systems: A Component-Based Modeling Language in 7th MEMOCODE. IEEE Computer Society, 2009.
• 3: M. Bozzano, A. Cimatti, J.-P. Katoen, V. Y. Nguyen, T. Noll, M. Roveri, The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems in 28th SAFECOMP. Springer, 2009.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Verification

General Terms:
Design, Performance, Reliability, Verification

Keywords:
aadl, dependability, model checking, performability, reliability