-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Signed-off-by: Enrico Ghiorzi <[email protected]>
- Loading branch information
1 parent
a82b22b
commit b2ba685
Showing
1 changed file
with
60 additions
and
2 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,2 +1,60 @@ | ||
# scan | ||
SCAN statistical model checker | ||
# SCAN | ||
|
||
SCAN (StatistiCal ANalyzer) is a statistical model checker | ||
designed to verify large concurrent systems | ||
that defy classic verification techniques. | ||
|
||
## Developement status | ||
|
||
SCAN is currently in developement at DIBRIS, University of Genoa (UniGe) | ||
in the context of the [CONVINCE project](https://convince-project.eu/). | ||
There is no released version yet. | ||
|
||
## Formalism | ||
|
||
SCAN uses Channel Systems (CS) as models, | ||
and Metric Temporal Logic (MTL) as property specification language. | ||
|
||
## Modeling specification languages | ||
|
||
SCAN is being developed to accept models specified in multiple, rich modeling languages. | ||
At the moment the following languages are planned or implemented: | ||
|
||
- [x] State Charts specified in SCXML format. | ||
- [ ] Promela | ||
- [ ] JANI | ||
|
||
## Build instructions | ||
|
||
Currently, the only way to use SCAN is to build it from sources. | ||
|
||
### Install a Rust toolchain. | ||
|
||
The easiest and recommended way is to do so by installing [Rustup](https://rustup.rs/) | ||
either following the instructions on its homepage or through your OS's package manager. | ||
|
||
### Clone and compile | ||
|
||
Clone the repo and enter its root folder. | ||
From there, compile SCAN with | ||
|
||
``` | ||
$ cargo build --release | ||
``` | ||
|
||
(without the `--release` flag, the compiler will build in debug mode). | ||
|
||
Then, run SCAN with either | ||
|
||
``` | ||
$ cargo run --release -- --help | ||
``` | ||
|
||
or | ||
|
||
|
||
``` | ||
$ target/release/scan --help | ||
``` | ||
|
||
and the CLI help will show the available functionalities and commands' syntax. |