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

In [1], HASL an expressive temporal logic was introduced in order to analyse stochastic and hybrid discrete event systems. Its formulas are described by a Linear Hybrid Automaton (LHA) and an expression involving state variables and using path and stochastic operators.

This logic is supported by Cosmos which performs statistical model checking of (ordinary or coloured) stochastic Petri nets with general distributions. The main algorithm of this tool randomly simulates the net according to its stochastic semantics and synchronises it with the execution of the automaton of the formula. During the synchronisation, it evaluates the expression of the formula providing a numerical (or boolean) value per trajectory. A statistical procedure decides when to stop the simulation and produces a confidence interval for a HASL expression.

The tool Cosmos consists of about 22000 lines of C++ code. The tool relies on code generation to perform efficient simulation. It is divided into three main parts:

Cosmos includes a family of statistical methods depending on the nature of the formula and the assumptions on the model. If the formula is boolean and corresponds to a comparison between the probability of an event and a threshold, it applies sequential hypothesis testing, a very efficient method where the number of generated trajectories is variable depending on the successive outputs. If the formula is numerical, it applies either a sequential method based on the Chow-Robbins bounds or several static methods where the number of trajectories is fixed in advance. More precisely, when the formula returns a probability (and thus corresponding to a Bernoulli distribution), it uses Clopper-Pearson bounds. When the formula returns the expectation of a bounded random variable, it uses the Chernoff-Hoeffding bounds. In the general case, it is based on the standard Gaussian approximation related to the average of independent and identically distributed random variables.

Cosmos has been successfully applied in the context of flexible manufacturing systems [1] and biological networks [11]. In addition, it has also been customised in order to address the challenges raised by different projects: