Uppaal SMC tutorial

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

149 Citationer (Scopus)
551 Downloads (Pure)

Resumé

This tutorial paper surveys the main features of Uppaal SMC, a model checking approach in Uppaal family that allows us to reason on networks of complex real-timed systems with a stochastic semantic. We demonstrate the modeling features of the tool, new verification algorithms and ways of applying them to potentially complex case studies.
OriginalsprogEngelsk
TidsskriftInternational Journal on Software Tools for Technology Transfer
Vol/bind17
Udgave nummer4
Sider (fra-til)397-415
Antal sider19
ISSN1433-2779
DOI
StatusUdgivet - 6 jan. 2015

Fingerprint

Model checking
Semantics

Citer dette

@article{56df82890c2b4710badf3f6db00aefe1,
title = "Uppaal SMC tutorial",
abstract = "This tutorial paper surveys the main features of Uppaal SMC, a model checking approach in Uppaal family that allows us to reason on networks of complex real-timed systems with a stochastic semantic. We demonstrate the modeling features of the tool, new verification algorithms and ways of applying them to potentially complex case studies.",
keywords = "Uppaal, Timed automata, model checking, statistical model checking, stochastic, Dynamical, Probabilistic",
author = "Alexandre David and Larsen, {Kim Guldstrand} and Axel Legay and Marius Mikučionis and Poulsen, {Danny B{\o}gsted}",
year = "2015",
month = "1",
day = "6",
doi = "10.1007/s10009-014-0361-y",
language = "English",
volume = "17",
pages = "397--415",
journal = "International Journal on Software Tools for Technology Transfer",
issn = "1433-2779",
publisher = "Physica-Verlag",
number = "4",

}

Uppaal SMC tutorial. / David, Alexandre; Larsen, Kim Guldstrand; Legay, Axel; Mikučionis, Marius; Poulsen, Danny Bøgsted.

I: International Journal on Software Tools for Technology Transfer, Bind 17, Nr. 4, 06.01.2015, s. 397-415.

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

TY - JOUR

T1 - Uppaal SMC tutorial

AU - David, Alexandre

AU - Larsen, Kim Guldstrand

AU - Legay, Axel

AU - Mikučionis, Marius

AU - Poulsen, Danny Bøgsted

PY - 2015/1/6

Y1 - 2015/1/6

N2 - This tutorial paper surveys the main features of Uppaal SMC, a model checking approach in Uppaal family that allows us to reason on networks of complex real-timed systems with a stochastic semantic. We demonstrate the modeling features of the tool, new verification algorithms and ways of applying them to potentially complex case studies.

AB - This tutorial paper surveys the main features of Uppaal SMC, a model checking approach in Uppaal family that allows us to reason on networks of complex real-timed systems with a stochastic semantic. We demonstrate the modeling features of the tool, new verification algorithms and ways of applying them to potentially complex case studies.

KW - Uppaal

KW - Timed automata

KW - model checking

KW - statistical model checking

KW - stochastic

KW - Dynamical

KW - Probabilistic

U2 - 10.1007/s10009-014-0361-y

DO - 10.1007/s10009-014-0361-y

M3 - Journal article

VL - 17

SP - 397

EP - 415

JO - International Journal on Software Tools for Technology Transfer

JF - International Journal on Software Tools for Technology Transfer

SN - 1433-2779

IS - 4

ER -