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

Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › peer review

390 Citationer (Scopus)

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

Originalsprog	Engelsk
Tidsskrift	International Journal on Software Tools for Technology Transfer
Vol/bind	17
Udgave nummer	4
Sider (fra-til)	397-415
Antal sider	19
ISSN	1433-2779
DOI	https://doi.org/10.1007/s10009-014-0361-y
Status	Udgivet - 6 jan. 2015

Adgang til dokumentet

10.1007/s10009-014-0361-y

preprintIndsendt manuskript, 1,32 MB

AUB Link

Søg efter materialet i Aalborg Universitetsbiblioteks søgemaskine

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

Citationsformater

@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 = "Physica-Verlag",

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

Adgang til dokumentet

AUB Link

Fingeraftryk

Projekter

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

Citationsformater