Uppaal SMC tutorial

Research output: Contribution to journalJournal articleResearchpeer-review

155 Citations (Scopus)
571 Downloads (Pure)

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.
Original languageEnglish
JournalInternational Journal on Software Tools for Technology Transfer
Volume17
Issue number4
Pages (from-to)397-415
Number of pages19
ISSN1433-2779
DOIs
Publication statusPublished - 6 Jan 2015

Fingerprint

Model checking
Semantics

Keywords

  • Uppaal
  • Timed automata
  • model checking
  • statistical model checking
  • stochastic
  • Dynamical
  • Probabilistic

Cite this

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

In: International Journal on Software Tools for Technology Transfer, Vol. 17, No. 4, 06.01.2015, p. 397-415.

Research output: Contribution to journalJournal articleResearchpeer-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 -