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 .
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 2 shows an LHA which measures the difference of memory usage.
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.To cite COSMOS, please use the most recent article from Perfomance Evaluation 2015
(BibTeX)
Lastest Version (Released on 29/06/2017)