Cosmos

Overview

Entry last updated: 2015/11/18
Entry last validated: 2015/11/18

Tool homepage: http://www.lsv.ens-cachan.fr/Software/cosmos/

Tool availability: Free of charge

Tool Features

Petri Nets Supported (see also help on terminology)

Place/Transition Nets
Stochastic Petri Nets
Stochastic Symmetric Nets

Components (see also help on terminology)

Fast Simulation
Interchange File Format
Rare Event Simulation

Environments

PC, Linux
Macintosh, Mac OS X

Tool Description

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 developped by searchers of LSV and LACL and was partially supported by the ANR project Check-bound .

Contact Information

Benoit Barbot
LACL, UniversitÈ Paris-Est CrÈteil Val de Marne
61 avenue du GÈnÈral de Gaulle
94010 CrÈteil Cedex 
France

Phone:  Remember country code
Fax:    Remember country code
E-mail: benoit.barbot@u-pec.fr

Other Remarks

The maintainers of this page