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:
The parsing and code generation part reads the input files and the command line to build data structures for the net and the automaton. Then optimised C++ code simulating both the synchronised behaviour of the net and the automaton is generated. The resulting code is compiled by a C++ compiler and linked with the simulator library. The resulting binary is the simulator program.
The simulator library implements the core algorithm for synchronisation. It also implements the stochastic generation of events using the pseudo random number generator provided by the boost library and handles these events in an event queue.
The server part launches several copies of the simulator and aggregates their results. According to statistical parameters, a procedure decides whether enough trajectories have been simulated and stops all simulators when needed. Then, HASL expressions are evaluated and several output files are produced according to options. The computation of confidence intervals uses the boost library for the computation of quantiles of the normal distribution function and binomial distribution.
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: