Uppaal SMC tutorial

Alexandre David; Kim Guldstrand Larsen; Axel Legay; Marius Mikučionis; Danny Bøgsted Poulsen

doi:10.1007/s10009-014-0361-y

Uppaal SMC tutorial

Alexandre David, Kim Guldstrand Larsen, Axel Legay, Marius Mikučionis, Danny Bøgsted Poulsen

Research output: Contribution to journal › Journal article › Research › peer-review

433 Citations (Scopus)

2437 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 language	English
Journal	International Journal on Software Tools for Technology Transfer
Volume	17
Issue number	4
Pages (from-to)	397-415
Number of pages	19
ISSN	1433-2779
DOIs	https://doi.org/10.1007/s10009-014-0361-y
Publication status	Published - 6 Jan 2015

Keywords

Uppaal
Timed automata
model checking
statistical model checking
stochastic
Dynamical
Probabilistic

Access to Document

10.1007/s10009-014-0361-y

preprintSubmitted manuscript, 1.32 MB

AUB Link

Search for the material in Aalborg University Library's search engine

CASSTING: Collective Adaptive System SynThesIs using Non-zero-sum Games
Larsen, K. G. (Project Manager), Skou, A. (Project Participant), David, A. (Project Participant) & Srba, J. (Project Participant)
FP7 STREP
01/04/2013 → 31/03/2016
Project: Research
SENSATION: Self Energy-Supporting Autonomous Computation
Larsen, K. G. (Project Manager), Hansen, R. R. (Project Participant), Koch, P. (Project Participant), Nielsen, B. (Project Participant) & Skou, A. (Project Participant)
FP7 FET Proactive
01/10/2012 → 30/09/2015
Project: Research
MBAT: Model-based Analysis and Testing of Embedded Systems
Nielsen, B. (Project Participant), Larsen, K. G. (Project Participant), David, A. (Project Participant), Mikučionis, M. (Project Participant) & Skou, A. (Project Participant)
Artemis JU
01/11/2011 → 31/10/2014
Project: Research

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{\v c}ionis and Poulsen, {Danny B{\o}gsted}",

year = "2015",

month = jan,

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 = "Springer",

number = "4",

}

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

SN - 1433-2779

VL - 17

SP - 397

EP - 415

JO - International Journal on Software Tools for Technology Transfer

JF - International Journal on Software Tools for Technology Transfer

IS - 4

ER -

Uppaal SMC tutorial

Abstract

Keywords

Access to Document

AUB Link

Fingerprint

Projects

CASSTING: Collective Adaptive System SynThesIs using Non-zero-sum Games

SENSATION: Self Energy-Supporting Autonomous Computation

MBAT: Model-based Analysis and Testing of Embedded Systems

Cite this