COMPASS 3

The COMPASS 3 project aims to improve the overall quality of the toolset, and consolidate all the previous improvements of past COMPASS projects.

Objectives

  1. Provide a consolidated definition of the syntax and semantics of the SLIM language, by incorporating selected constructs from previous projects, and resolve existing semantics issues and discrepancies between different tools.
  2. Enhance the COMPASS V&V functionality by upgrading the verification engines to more recent state-of-the-art routines developed in formal verification.
  3. Resolve existing issues of the user interface, and update it to expose the new functionality provided by the verification engines.
  4. Improve the overall software quality, and upgrade the software to use more recent software packages and libraries, for better maintainability.
  5. Improve the dissemination of the results, by restructuring the projects’ web sites, in order to offer a clear and unified picture of the COMPASS initiative and of related project and achievements, and by providing additional material such as a tutorial.

Overview

Project Consolidation

Over the past few years, various COMPASS-related projects have provided changes and new features to the toolset. Part of the COMPASS 3 project is aimed towards consolidating those changes into a new version of COMPASS. Below is a figure that shows the historic relation between the past projects, that COMPASS 3 aim to consolidate.

compass_projUpdated syntax and semantics

Another aim of COMPASS 3 is to bring the SLIM language closer to the AADL standard, and provide a better integration of the language enhancements of past projects.

Support has been added for the AADL property system, which allows many of the SLIM-specific constructs used before to be represented in an AADL compliant way. This also opens up the path towards the use of AADL tooling such as OSATE for working with COMPASS models.

Improved backend

The backend tools are updated, upgrading them to their latest versions, and make use of new state-of-the-art verification engines. The nuXmv model checker is integrated which provides new IC3-based verification engines. The addition of OCRA/nuXmv furthermore introduces compositional reasoning.

Code quality is improved by making the code compliant with the PEP8 standard, is well as improving the COMPASS test suite, including making use of continuous integration.

Updated documentation and examples

The COMPASS Manual and SLIM specifications are updated to reflect the current state of the art. Furthermore, a new tutorial will be made available to make it easier to start using the toolset as a whole. The tutorial will provide a step by step approach to explaining how the toolset works and what its capabilities are. The suite of examples provided with the toolset will also be updated, to reflect the updated syntax of the SLIM language and provide a more consistent view on its capabilities.