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

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 developed by searchers of Inria, at LSV and LACL.

Simulink models and Cosmos

Cosmos can simulate models given in the Simulink model, and also simulate a model described using, at the same time, a DESP (usually, a GSPN) and a Simulink model that may exchange information. Click here for more details, alongside an example of the verification of a double heater.

To cite Cosmos, please refer to the following paper:
P. Ballarini, B. Barbot, M. Duflot, S. Haddad and N. PekerginHASL: A New Approach for Performance Evaluation and Model Checking from Concepts to Experimentation Performance Evaluation 90, pages 53-77, 2015.

The current developer is BenoƮt Barbot.
Yann Duplouy, Hilal Djafri and Paollo Ballarini have contributed to the development.
Marie Duflot, Serge Haddad and Nihal Pekergin have contributed to the theoretical design of the tool.