New
Watch the demo tutorial on YouTube!
Download and play with the most recent version bip-smc-1.1!
Overview
This page presents an overview of the BIP-SMC tool, a Statistical Model Checking engine for the BIP framework.
Tool Architecture
How to install and run the tool
Requirements :
- Linux
- Java 1.6
To install the tool follow those steps :
- First, download, extract and install BIP. The model checker works with the old and the new version of BIP.
- Download and extract the Statistical Model Checker archive.
- lets call SMC_HOME the obtained directory path. It contains :
- lib/ directory that contains libraries used by the tool,
- bin/ directory that contains the tool binaries,
- examples/ directory that contains BIP examples,
- setup.sh script to set up the environment, and
- README file that describes the tool.
- To use the tool on command line, you have to source the setup.sh. This will add the binary to you path and let you use it from any location :
$ source $SMC_HOME/setup.sh
- First, you have to Build your BIP example with respect to the BIP version you are using.
- Then, to verify it, you have to use a command line prototype :
$ sbip [-htest|-pestim] [Formula] [Delta] [Alpha] [Beta] [-bip1|-bip2] [BIP Executable]
where :
- -htest is to specify if you want to do hypothesis testing or probability estimation,
- [Formula] is a PB-LTL formula,
- [Delta], [Alpha] and [Beta] defines the level of confidence of the tool,
- -bip1 is to specify which version of BIP you are going to sue, and
- [Executable] is the BIP binary you want to verify.
PB-LTL syntax
The PB-LTL Logic is a classic LTL formula f wrapped in:
- P>=theta[ f ] a probabilistic operator parametrized by a probability theta (to do hypothesis testing), or
- P=?[ f ] a probabilistic operator without parameter (to do probability estimation).
The implemented bounded temporal operators are :
- N : Next
- U{i} : Until
- F{i} : Eventually
- G{i} : Always
Here i is the bound of the temporal operators. For example, G{1000} stand for classical Always but for bounded traces of length 1000.
As operand for the temporal operators you can write classical Boolean formulas on system state variables. For this first prototype, you can only use conjunction and disjunction (&&, ||). The state variables of a specific component are written in this way : ComponentName.VariableName.
Note that in this version, it is not possible to use nested temporal operators in a formula.
Running Example : Precision Time Protocol (PTP)
PTP Description
The Precision Time Protocol has been defined to synchronize clocks of several computers interconnected over an network. The protocol rely on multicast communication to distribute a reference time from an accurate clock (the master) to all other clocks in the network (the slaves) combined with individual offset correction, for each slave, according to its specific round-trip communication delay to the master. We present below the abstract stochastic model of the PTP protocol between a device and the server in the HCS [1] case study. The model consists of two (deterministic) application components respectively, the master and the slave clocks, and two probabilistic components, the media, which are abstraction of the communication network between the master and the slave.
Running Steps
- Under a terminal, build the bip sources with respect to the used bip version (the ptp example uses old bip version).
- Run the tool using the following command line :
$ sbip -htest "P>=0.65[G{1000}(abs(Master.tm-Slave.ts)<=90)]" 0.05 0.00001 0.00001 -bip1 ptp.bip.x
This command is to check if the deviation between master and slave clocks is always under 90 milliseconds with a probability 0.7 (0.65 + 0.05). To express this requirement we use the following PB-LTL Formula : "P>=0.65[G{1000}(abs(Master.tm-Slave.ts)<=90)]".
After the P-LTL formula, you should specify the Delta parameter (in this case 0.05) which is the half-width of the indifference region, the Alpha and Beta (in this case both are 0.00001) that represents the strength or the confidence level of the test.
Finally, you should specify the used bip version and the binary of the BIP model to verify, in this case for example -bip1 ptp.bip.x since it uses old bip version.
Benchmarks
Virtual Links latency analysis in AFDX (See [2] for details)
Two switchs :
Four switchs :
Six switchs :
Synchronization precision analysis for PTP protocol (See [1] for details)
Synchronization Results for Bound equal 50µs
Weighted Fair Queuing 50,20,20,10 | Weighted Fair Queuing 40,20,20,10 |
Weighted Fair Queuing 20,30,10,40 | Fixed Priority |
Synchronization Results for Bound in [0,140] µs
Fixed Priority | Weighted Fair Queuing 50,20,20,10 |
Projects
Contact
This tool is developed and maintained by Ayoub Nouri: ayoub.nouri[at]imag.fr
Related Paper
[1] Ananda Basu, Saddek Bensalem, Marius Bozga, Benoît Caillaud, Benoît Delahaye, Axel Legay: Statistical Abstraction and Model-Checking of Large Heterogeneous Systems. FMOODS/FORTE 2010.
[2] Ananda Basu, Saddek Bensalem, Marius Bozga, Benoît Delahaye, Axel Legay, Emmanuel Sifakis: Verification of an AFDX Infrastructure Using Simulations and Probabilities. RV 2010.
[3] Saddek Bensalem, Marius Bozga, Benoît Delahaye, Cyrille Jégourel, Axel Legay, Ayoub Nouri: Statistical Model Checking QoS Properties of Systems with SBIP. ISoLA 2012.
[4] Ayoub Nouri, Saddek Bensalem, Marius Bozga, Benoit Delahaye, Cyrille Jégourel, and Axel Legay: Statistical model checking QoS properties of systems with SBIP, International Journal on Software Tools for Technology Transfer, 1-15.
[5] Balaji Raman, Ayoub Nouri, Deepak Gangadharan, Marius Bozga, Ananda Basu, Mayur Maheshwari, Axel Legay, Saddek Bensalem, and Samarjit Chakraborty : Stochastic Modeling and Performance Analysis of Multimedia SoCs, SAMOS’13, Samos Greece.