# SBIP : A Statistical Model Checking Extension for BIP framework

### New

Watch the demo tutorial on YouTube!

### Overview

This page presents an overview of the BIP-SMC tool, a Statistical Model Checking engine for the BIP framework.

### 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.
• 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.

### 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.

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

### 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.

## titre documents joints

### Tool Archive

30 April 2013
info document : TGZ
9.9 Mb