Statistical model checking in Uppaal: lets practice

Alexandre David, K.G. Larsen, Axel Legay, Marius Mikučionis

    Research output: Contribution to conferencePaper

    38 Downloads (Pure)


    Statistical model-checking is a recent technique used for both verification and performance analysis of hybrid systems. It does not suffer from decidability issues or state-space explosion compared to traditional model-checking. Furthermore, it is applicable to more powerful formalisms such as stochastic hybrid automata. Its principle is simple so how simple is it really to make it work in practice? In this extended abstract, we raise a number of practical issue, some of them disconnected from the underlying theory, and show how they are addressed in Up- paal SMC.
    Original languageUndefined
    Publication statusPublished - Sep 2013
    EventFirst Workshop on Statistical Model Checking - INRIA Rennes, Rennes, France
    Duration: 23 Sep 201323 Sep 2013


    WorkshopFirst Workshop on Statistical Model Checking
    Abbreviated titleSMC 2013


    • IR-101819
    • EC Grant Agreement nr.: FP7/318003
    • EC Grant Agreement nr.: FP7/2007-2013

    Cite this