COMPASS: Correctness, Modeling and Performance of Aerospace Systems

COMPASS is an international research effort aiming to ensure system-level correctness, safety, dependability and performability of on-board computer-based aerospace systems COMPASS 3.0 brings together the results of various development projects since the original inception of COMPASS (this says nothing)

Application domain/field

• Aerospace systems
• Model checking

Type of tool

Framework

Expected input

• Model
• Properties

Format:

SLIM language (dialect of AADL) http://www.compass-toolset.org/docs/slim-specification.pdf

Expected output

Depends on the tool/back-end that is used to analyze the model.

Internals

The provided model is internally converted into a symbolic model and to a Markov chain. Properties are automatically translated into temporal logic formulas. COMPASS then provides many different ways to analyse these model/properties such as:

• nuXmv for correctness checking
• OCRA for contract-based analysis
• IMCA and MRMC for performance analysis by probabilistic model checking
• slimsim for statistical model checking
• xSAP for safety analysis