COSMOS

COSMOS is a statistical model checker for the Hybrid Automata Stochastic Logic (HASL). It takes two inputs: a Discrete Event Stochastic Process (DESP) expressed in terms of a Stochastic Petri Nets (with generally distributed Timed transitions) and a temporal property, expressed in terms of a Linear Hybrid Automaton (LHA). The output of the computation is a confidence-interval estimation of the measure encoded by the considered  LHA. 

The use of Linear Hybrid Automata as machineries to simultaneously select relevant paths and measure relevant quantities "recorded" along the selected paths, essentially unifies the probabilistic model checking verification with reward-based analysis in a single tool yielding a powerful formalism which extends the expressiveness of existing stochastic logic (e.g. CSL, asCSL, CSL-TA, CSRL). 

For further informations look at COSMOS-webpage