COSMOS: a statistical model checker for the hybrid automata stochastic logic. This tool paper introduces Cosmos, a statistical model checker for the Hybrid Automata Stochastic Logic (HASL). HASL employs Linear Hybrid Automata (LHA), a gen eralization of Deterministic Timed Automata (DTA), to describe relevant 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), an 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.
Keywords for this software
References in zbMATH (referenced in 3 articles )
Showing results 1 to 3 of 3.
- Ballarini, Paolo; Duflot, Marie: Applications of an expressive statistical model checking approach to the analysis of genetic circuits (2015)
- Amparore, Elvio Gilberto; Ballarini, Paolo; Beccuti, Marco; Donatelli, Susanna; Franceschinis, Giuliana: Expressing and computing passage time measures of GSPN models with HASL (2013)
- Rohr, Christian: Simulative model checking of steady state and time-unbounded temporal operators (2013)