Room 206 (2nd floor, badged access)
14 juin 2019 - 14h00
Cosmos a quantitative verification tool for large stochastic systems
par Benoit Barbot de LACL, Universite Paris Est, Creteil
Abstract: Large family of systems can be modeled with stochastic processes, for example: waiting queue for network infrastructure, biological systems, road traffic flow, ...
Due to combinatorial explosion, analysis using exhaustive methods of such systems is intractable. More over it is often necessary to answer both; qualitative question like Does an unsafe state is reachable is the system ? and quantitative one like What is the throughput of a routing system ? The tool Cosmos is a statistical model checker implementing simulation methods for efficient verification of the HASL logic. This logic has been developed to take advantage of statistical model checking methods both for expressivity and efficient verification. In this talk we will present how Cosmos has been applied to the verification hybrid systems and to the uniform generation of time words.
