COMPASS

COMPASS (COrrectness, Modeling and Performance of AeroSpace Systems) is a toolset aiming to ensure system-level correctness, safety, dependability and performability of on-board computer-based aerospace systems. The COMPASS toolset provides an integrated model-based approach for System-Software Co-Engineering. It uses formal verification techniques, notably model checking, and originates from an ESA initiative dating back to 2008. The COMPASS 3.0 release brings together the results of various development projects since the original inception
of COMPASS. Namely, the AUTOGEF project focused on Fault Detection, Identification and Recovery (FDIR) and FDIR synthesis in the discrete domain; FAME focused on the FDIR development and Validation and Verification process and on fault propagation analysis; HASDEL extended formal analysis techniques in the domain of RAMS (Reliability, Availability, Maintainability and Safety) analysis, with a strong focus on timed aspects of the model; finally CATSY had the goal of improving the requirements specification process.

The COMPASS toolset provides a GUI as well as command-line scripts. The backend engines include the nuXmv model checker for correctness checking; OCRA for contract-based analysis; MRMC and IMCA for performance analysis using probabilistic model checking; slimsim for statistical model checking and xSAP for safety analysis. The COMPASS 3.0 distribution includes a user manual and a tutorial. Moreover, COMPASS 3.0 provides the following novel functionality:

• The input language, called SLIM (a variant of AADL) has been updated with the inclusion of the AADL property system, timed error models, non-blocking ports and separation of configuration and behavior.
• Properties can now be specified in three ways in COMPASS: by means of design attributes; as patterns; or as logical expressions. These methods range from ‘simple to use’ but less expressive, to ‘expert use’ but more expressive.
• SAT-based verification routines have been extended with K-Liveness verification, which typically outperforms older routines. Moreover, COMPASS offers the possibility to check Zenoness and clock divergence for timed models.
• COMPASS now supports the contract-based development and verification methodology. In particular, it can perform three types of analysis: contract validation, refinement checking, and contract tightening.
• Safety assessment functionality now includes Hierarchical Fault Tree Analysis, Fault Tree Evaluation and Verification. Moreover, COMPASS supports fault propagation analysis using Timed Failure Propagation Graphs (TFPG).
• Performability analysis can be carried out using numerical analysis for both Continuous-Time (CTMC) and Interactive (IMC) Markov Chains, the latter making it possible to analyze continuous-time stochastic models which exhibit non-determinism. Moreover, statistical model checking using Monte Carlo simulation can be used to analyze hybrid models containing clocks.