Statistical model checking in Uppaal: lets practice

Alexandre David; Kim G. Larsen; Axel Legay; Marius Mikučionis

Statistical model checking in Uppaal: lets practice

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

Research output: Contribution to conference › Paper

86 Downloads (Pure)

Abstract

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 language	English
Number of pages	7
Publication status	Published - Sept 2013
Event	1st Workshop on Statistical Model Checking, SMC 2013 - INRIA Rennes, Rennes, France Duration: 23 Sept 2013 → 23 Sept 2013 Conference number: 1

Workshop

Workshop	1st Workshop on Statistical Model Checking, SMC 2013
Abbreviated title	SMC
Country/Territory	France
City	Rennes
Period	23/09/13 → 23/09/13

Keywords

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

Access to Document

ArticleFinal published version, 196 KB

Cite this

@conference{48cebcf7160046ff9b9659021e91a5cf,

title = "Statistical model checking in Uppaal: lets practice",

abstract = "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.",

keywords = "EC Grant Agreement nr.: FP7/318003, EC Grant Agreement nr.: FP7/2007-2013",

author = "Alexandre David and Larsen, {Kim G.} and Axel Legay and Marius Miku{\v c}ionis",

year = "2013",

month = sep,

language = "English",

note = "1st Workshop on Statistical Model Checking, SMC 2013, SMC ; Conference date: 23-09-2013 Through 23-09-2013",

}

TY - CONF

T1 - Statistical model checking in Uppaal: lets practice

AU - David, Alexandre

AU - Larsen, Kim G.

AU - Legay, Axel

AU - Mikučionis, Marius

N1 - Conference code: 1

PY - 2013/9

Y1 - 2013/9

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

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

KW - EC Grant Agreement nr.: FP7/318003

KW - EC Grant Agreement nr.: FP7/2007-2013

M3 - Paper

T2 - 1st Workshop on Statistical Model Checking, SMC 2013

Y2 - 23 September 2013 through 23 September 2013

ER -

Statistical model checking in Uppaal: lets practice

Abstract

Workshop

Keywords

Access to Document

Fingerprint

Cite this