COSMOS project link

Winstead via FLUENT Verification Project

Fri, 06 Sep 2019 14:14:30 -0600

!!FLUENT Verification Project

#^Cosmos Website

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...

#COSMOS #tools #software #HASL

Zhen Zhang

Fri, 20 Sep 2019 14:26:51 -0600

@Winstead This STORM page shows various different
input modeling languages and their intermediate format JANI for conversion between them: #^http://www.stormchecker.org/documentation/usage/languages.html