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

Type of tool


Expected input


SLIM language (dialect of AADL)

Expected output

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


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:
Framework Model checking Probabilistic


Related papers


Last publication date

4 April 2019

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.