Introduction

SCAN (StatistiCal ANalyzer) is a statistical model checker designed to verify large concurrent systems for which standard verification techniques do not scale.

It features:

• SCXML as input language (support for other languages is underway)
• Past MTL as property specification language
• State/event dense time traces

SCAN is currently under developement at DIBRIS, University of Genoa in the context of the CONVINCE project.

While SCAN can also be as a standalone model checker, it closely integrates with the other tools in the CONVINCE toolchain. In particular, AS2FM can target the SCXML format accepted by SCAN, to make verification of robotic systems more accessible to robotic systems developers.

API docs for the library crates.

Installation

Build prerequisites

SCAN is entirely written in Rust, so, to build it, you need to install a recent version of the Rust toolchain. The easiest and recommended way to do so is by installing rustup either following the instructions on its homepage or through your OS's package manager. Do not forget to set your PATH correctly, if required.

Installing with Cargo

To install and use SCAN on your system, the easiest way is to use the cargo install command, with:

cargo install --git https://github.com/convince-project/scan

Cargo will build and install SCAN on your system, after which it can be used as a command-line tool.

Successively, the same command updates SCAN to the latest version.

The User Interface

SCAN provides a command line interface.

To print the help screen, use

scan --help

which will show the available functionalities and commands' syntax.

The general syntax to run SCAN is

scan [OPTIONS] [MODEL]

where MODEL is the path to the directory containing the model's scxml files. As the default directory is the current one, just invoking scan inside a model's directory starts the verification with default settings. If the model has a main xml file, passing its path instead of the folder's allows for finer control over which processes the model is using and where their definition can be found.

Settings and Options

SCAN accepts the following parameters:

• --format sets which model specification format is being used. Possible values: [scxml|jani]. Defaults to scxml as SCXML is the better-supported format. Support for the JANI format is in progress.
• --confidence sets the statistical confidence that the produced result is accurate.
• --precision sets the target precision of the result.

Toghether, --confidence and --precision determine how many executions are required to be performed.

The following parameters are to be set by the developer according to the use case:

• --length sets the maximum length a trace can reach before the execution is stopped.
• --duration sets the maximum duration (in model time) that the execution can take before being stopped.

As these settings may vary depending on the use case, SCAN sets reasonably large default values, but they can be changed if necessity arises.

The following option are available:

• --traces has all the traces produced during verification saved in a ./traces_NN/ folder, with NN progressive indexing, and further classified into success/, failure/<FAILED_PROPERTY> and undetermined/ sub-folders based on the outcome of the execution. Traces are saved into gz-compressed csv format. Since traces can take up a large amount of disk space, the option is disabled by default and care is reccommended when enabling it.
• --ascii enables an ascii-compatible interface, in case the terminal has no Unicode support. It is disabled by default as Unicode-compatible terminals are relatively common.

Logging

It can be helpful to run SCAN with logging activated. Use

RUST_LOG=<LOG_LEVEL> scan [OPTIONS] [MODEL]

where LOG_LEVEL=[error|warn|info|debug|trace] (from the highest-level to the lowest-level log entries).