SCAN
SCAN (StatistiCal ANalyzer) is a statistical model checker designed to verify large concurrent systems for which standard verification techniques do not scale.
Development status
SCAN is currently under development at DIBRIS, University of Genoa (UniGe) in the context of the CONVINCE project.
Documentation
User documentation: The SCAN Book.
API docs for the library crates:
Formalism
Internally, SCAN uses Channel Systems (CS) as models,[^1] and past Metric Temporal Logic (pMTL) as property specification language.
[^1]: Baier, C., & Katoen, J. (2008). Principles of model checking. MIT Press.
SCAN is being developed to accept models specified in multiple, rich modeling languages. At the moment the following languages are planned or (partially) implemented:
- State Charts specified in SCXML format.
- Promela
- JANI
Installation
Currently, the only way to obtain SCAN is to build it from sources.
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.
Follow the instructions from the Build prerequisites section to install the required build dependencies.
Then, install SCAN directly from crates.io with:
cargo install smc_scan --locked
Cargo will build and install SCAN on your system
(the --locked option is not required,
but it is recommended as it improves build reproducibility
by enforcing the use of specified versions for dependencies).
For advanced installation options, refer to the Install section of the SCAN Book.
Usage
After installation, SCAN can be used as a CLI tool. To print the help screen, use
scan --help
which will show the available functionalities and commands' syntax.
To verify all specified properties over a model, for example, use:
scan <MODEL> verify --all
where MODEL is the path to your model file or folder.
For an in-depth documentation of the user interface, refer to the Interface section of the SCAN Book.
Development
For development's purposes, you will want to build and run SCAN from source code.
Use Cargo's usual build and run commands for that.
For example, from the repo's root folder, build SCAN with
cargo build
Cargo, Rust's build manager, will take care of importing the required dependencies.
Run SCAN via Cargo with
cargo run -- [ARGS]
or by running the executable file directly, with
target/debug/scan [ARGS]
Install your local version of Scan on your system for more ease of use, with:
cargo install --path <SCAN_REPO_PATH>
To build SCAN's documentation API (with suggested flags) and have it open in a browser tab, run:
cargo doc --no-deps --workspace --open
Run all unit and integration tests with:
cargo test --workspace