Tools
The envisioned COMPASS integrated platform toolset comprises of several model validation and reduction tools, all integrated together to accept SLIM models. The uses tools are described below.
Formal Safety Analysis Platform
FSAP is developed at Fondazione Bruno Kessler, Italy. It can analyze dynamic systems, in particular it supports both permanent (steady-state) failure modes (once failed, always failed), and sporadic or transient (intermittent) ones, that is, when faults are allowed to occur sporadically (e.g., a sensor showing an invalid reading for a limited period of time), or when repairing is possible.
Model Based Planner
MBP is developed at Fondazione Bruno Kessler, Italy. The Model Based Planner (MBP) is a system designed to perform plan synthesis, plan validation and plan/domain simulation in non-deterministic domains.
Markov Reward Model Checker
MRMC tool is developed at the Software Modeling and Verification (MOVES) group at RWTH Aachen University (Germany) and the Formal Methods & Tools group at University of Twente (the Netherlands). It is a model checker for discrete-time and continuous-time Markov reward models. It supports reward extensions of PCTL and CSL (PRCTL and CSRL), and allows for the automated verification of properties concerning long-run and instantaneous rewards as well as cumulative rewards.
NuSMV
NuSMV is an open source reimplementation and extension of SMV, the first model checker based on BDDs led by Fondazione Bruno Kessler, Italy. It has been designed to be an open architecture for model checking, which can be reliably used for the verification of industrial designs, as a core for custom verification tools, as a testbed for formal verification techniques.
Requirements Analysis Tool
RAT is a tool for requirements validation developed at the Fondazione Bruno Kessler, Italy. It is used to formalize functional requirements, simulate them and analyse them for consistency, completeness, correctness and realizability.
Sigref
Sigref is a novel tool for the bisimulation minimization of labelled transition systems devenloped at the University of Freiburg, Germany. The novelty of Sigref is that it is designed for symbolic representations of labelled transition systems (i.e., using BDDs). Sigref supports several notions of bisimulation equivalence, among which are the most prominent ones, e.g., strong, weak, and branching bisimulation.
