COMPASS Tool Tutorials

We have a number of tools available to help get started with the different features of the COMPASS tool. More polished versions will be produced later in the project: the aim here is to give a good impression of what can be done now.

We welcome feedback on the videos, please use the contact details on the Home page to do so.

The current version of the COMPASS Tool can be found on Sourceforge.

Clicking on each title will expand to show the video inline. You may need to run the video full-screen to see the full detail.

Core COMPASS Tutorials

+ Getting Started: How to start Symphony and import public projects - Getting Started: How to start Symphony and import public projects

+ Working with the debugger - Working with the debugger

+ Working with the model checker - Working with the model checker

+ How to select an element from a set of values in the debugger - How to select an element from a set of values in the debugger

+ Using the Symphony theorem prover with CML - Using the Symphony theorem prover with CML

+ Using the Symphony theorem prover to discharge CML proof obligations - Using the Symphony theorem prover to discharge CML proof obligations

+ Refinement with the Symphony tool - Refinement with the Symphony tool

+ Translating SysML to CML (S2C) - Translating SysML to CML (S2C)

+ Installing the SysML to CML Generator - Installing the SysML to CML Generator

+ Using the SysML to CML Generator - Using the SysML to CML Generator

+ Symphony Collaborative Modeling - Symphony Collaborative Modeling

+ Using the Collaboration Plugin - Using the Collaboration Plugin

+ Symphony Distributed Simulation - Symphony Distributed Simulation

Model Checking Tutorials

+ Model checking tools: Installation - Model checking tools: Installation

+ The model checking perspective - The model checking perspective

+ Deadlock analysis - Deadlock analysis

+ Model Checking Analysis of Bit Register - Model Checking Analysis of Bit Register

+ Model Checking Analysis: Three examples - Model Checking Analysis: Three examples

RT Tester Tutorials

+ Getting started with the integrated RT Tester functionality - Getting started with the integrated RT Tester functionality

+ How create a new RT Tester project - How create a new RT Tester project

+ How to generate test procedures in RT Tester - How to generate test procedures in RT Tester

+ How to execute test procedures in RT Tester - How to execute test procedures in RT Tester

+ A demonstration of Passive Testing - A demonstration of Passive Testing

Fault Analysis Tutorials

+ Translating SysML to HiP-HOPS - Translating SysML to HiP-HOPS

+ The Fault-Tolerance Plugin - The Fault-Tolerance Plugin