SCAN (StatistiCal ANalyzer) is a statistical model checker designed to verify large concurrent systems for which standard verification techniques do not scale.
SCAN is currently under development at DIBRIS, University of Genoa (UniGe) in the context of the CONVINCE project.
User documentation: The SCAN Book.
API docs for the library crates:
Internally, SCAN uses Channel Systems (CS) as models,1 and past Metric Temporal Logic (pMTL) as property specification language.
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
Currently, the only way to obtain SCAN is to build it from sources.
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.
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 --lockedCargo 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.
After installation, SCAN can be used as a CLI tool. To print the help screen, use
scan --helpwhich will show the available functionalities and commands' syntax.
To verify all specified properties over a model, for example, use:
scan <MODEL> verify --allwhere 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.
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 buildCargo, 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 --openRun all unit and integration tests with:
cargo test --workspaceFootnotes
-
Baier, C., & Katoen, J. (2008). Principles of model checking. MIT Press. ↩