COSMOS : a Statistical Model Checker for the Hybrid Automata Stochastic Logic

Description

COSMOS is a statistical model checker for Hybrid Automata Stochastic Logic (HASL). HASL uses Linear Hybrid Automata (LHA), a generalization of Deterministic Timed Automata (DTA), to describe accepting execution paths of a Discrete Event Stochastic Process (DESP), a class of stochastic models which includes, but is not limited to, Markov chains. As a result, HASL verification turns out to be a unifying framework where sophisticated temporal reasoning is naturally blended with elaborate reward-based analysis. COSMOS takes as input a DESP (described in terms of a Generalized Stochastic Petri Net), a LHA and an expression Z representing the quantity to be estimated. It returns a confidence interval estimation of Z. COSMOS is written in C++ and is freely available to the research community. It is jointly developped by searchers of LSV and LACL and was partially supported by the ANR project Check-bound .

Example

Model

Figure 1 shows a GSPN modeling a shared memory system. Transitions "Arrive1" and "Arrive2" follow an exponential distribution, "Start1" and "Start2" are instantaneous, and "End1" and "End2" follow a uniform distribution.


Figure 1 : GSPN model of a shared memory system
File text of this example




Automaton and Formula

Figure 2 shows an LHA which measures the difference of memory usage.


Figure 2 : A Linear Hybrid Automaton (LHA) measuring differences of memory usage File text of this example


To compute the difference of memory usage, COSMOS needs the following HASL formula:
AVG(Last(OK))
This formula expresses the average value of the variable OK in the final state.
The input file formats of GSPN and LHA are described in this document.

Simulation

To start COSMOS on this example, first go to the directory Examples/SharedMemory from the Cosmos directory, then launch the binary with the following arguments:

cosmos sms_Unif.gspn sms_Unif.lha --width 0.01

Those arguments make COSMOS performs simulations until the confidence interval for the HASL formula has a width smaller than 0.01. COSMOS builds an internal representation of the model and the automaton, using code generation, and then starts the simulation.

Cosmos:

Start Parsing sms_Unif.gspn

Start Parsing sms_Unif.lha

Parsing OK.


Start building ...

Building OK.


START SIMULATION ...

Estimated value: 0.499119402985075

Confidence interval: [0.494143613790152 , 0.504095192179998]

Width: 0.00995157838984584

Confidence interval computed sequentially using Chows-Robbin algorithm.

Confidence level: 0.99

Total paths: 67000

Accepted paths: 67000

Time for simulation: 5.776912s

Total CPU time: 7.910013

Results are saved in 'Result.res'

The --help option can be used to show the list of available options.

COSMOS and CosyVerif

COSMOS is integrated inside the CosyVerif platform. This platform provides a graphical front end named Coloane allowing one to draw GSPN and LHA with a graphical editor. COSMOS reads the GRML file format used by CosyVerif, both for GSPN and LHA.

Figure 3 : Screen-shot of the graphical interface of CosyVerif running COSMOS


Stochastic Symmetric Net

COSMOS has been extended to use Stochastic Symmetric Net (SSN) in addition to GSPN allowing to build more compact models. The file format used by COSMOS for SSN is the GRML. Unfortunately the SSN formalism is not yet included in Coloane. You can find here a description on how to transform a symmetric net into a SSN.

References

To cite COSMOS, please use the most recent article from Perfomance Evaluation 2015 (BibTeX)

Download

cosmos_1.0.tar.gz

Lastest Version (Released on 29/06/2017)

Case studies

case studies

Current Developers

Benoît Barbot

Yann Duplouy

Past Developers

Hilal Djafri

Paolo Ballarini

About LSV