UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata

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

doi:10.4204/EPTCS.85.1

UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata

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

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

95 Citations (Scopus)

Abstract

This paper offers a survey of U PPAAL - SMC, a major extension of the real-time verification tool
U PPAAL. U PPAAL - SMC allows for the efficient analysis of performance properties of networks of
priced timed automata under a natural stochastic semantics. In particular, U PPAAL - SMC relies on
a series of extensions of the statistical model checking approach generalized to handle real-time
systems and estimate undecidable problems. U PPAAL - SMC comes together with a friendly user
interface that allows a user to specify complex problems in an efficient manner as well as to get
feedback in the form of probability distributions and compare probabilities to analyze performance
aspects of systems. The focus of the survey is on the evolution of the tool – including modeling and
specification formalisms as well as techniques applied – together with applications of the tool to case
studies.

Original language	English
Journal	Electronic Proceedings in Theoretical Computer Science
Volume	85
Pages (from-to)	1-16
Number of pages	17
ISSN	2075-2180
DOIs	https://doi.org/10.4204/EPTCS.85.1
Publication status	Published - 2012
Event	10th Workshop on Quantitative Aspects of Programming Languages and Systems - Tallinn, Estonia Duration: 31 Mar 2012 → 1 Apr 2012 Conference number: 10th

Conference

Conference	10th Workshop on Quantitative Aspects of Programming Languages and Systems
Number	10th
Country/Territory	Estonia
City	Tallinn
Period	31/03/2012 → 01/04/2012

Access to Document

10.4204/EPTCS.85.1

AUB Link

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

Cite this

@inproceedings{52d7fa028e4d42d4ba91e57760431bd1,

title = "UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata",

abstract = "This paper offers a survey of U PPAAL - SMC, a major extension of the real-time verification toolU PPAAL. U PPAAL - SMC allows for the efficient analysis of performance properties of networks ofpriced timed automata under a natural stochastic semantics. In particular, U PPAAL - SMC relies ona series of extensions of the statistical model checking approach generalized to handle real-timesystems and estimate undecidable problems. U PPAAL - SMC comes together with a friendly userinterface that allows a user to specify complex problems in an efficient manner as well as to getfeedback in the form of probability distributions and compare probabilities to analyze performanceaspects of systems. The focus of the survey is on the evolution of the tool – including modeling andspecification formalisms as well as techniques applied – together with applications of the tool to casestudies.",

author = "Petr Bulychev and Alexandre David and Larsen, {Kim Guldstrand} and Marius Miku{\v c}ionis and Poulsen, {Danny B{\o}gsted} and Axel Legay and Zheng Wang",

year = "2012",

doi = "10.4204/EPTCS.85.1",

language = "English",

volume = "85",

pages = "1--16",

journal = "Electronic Proceedings in Theoretical Computer Science",

issn = "2075-2180",

publisher = "Open Publishing Association",

note = "10th Workshop on Quantitative Aspects of Programming Languages and Systems ; Conference date: 31-03-2012 Through 01-04-2012",

}

TY - GEN

T1 - UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata

AU - Bulychev, Petr

AU - David, Alexandre

AU - Larsen, Kim Guldstrand

AU - Mikučionis, Marius

AU - Poulsen, Danny Bøgsted

AU - Legay, Axel

AU - Wang, Zheng

N1 - Conference code: 10th

PY - 2012

Y1 - 2012

N2 - This paper offers a survey of U PPAAL - SMC, a major extension of the real-time verification toolU PPAAL. U PPAAL - SMC allows for the efficient analysis of performance properties of networks ofpriced timed automata under a natural stochastic semantics. In particular, U PPAAL - SMC relies ona series of extensions of the statistical model checking approach generalized to handle real-timesystems and estimate undecidable problems. U PPAAL - SMC comes together with a friendly userinterface that allows a user to specify complex problems in an efficient manner as well as to getfeedback in the form of probability distributions and compare probabilities to analyze performanceaspects of systems. The focus of the survey is on the evolution of the tool – including modeling andspecification formalisms as well as techniques applied – together with applications of the tool to casestudies.

AB - This paper offers a survey of U PPAAL - SMC, a major extension of the real-time verification toolU PPAAL. U PPAAL - SMC allows for the efficient analysis of performance properties of networks ofpriced timed automata under a natural stochastic semantics. In particular, U PPAAL - SMC relies ona series of extensions of the statistical model checking approach generalized to handle real-timesystems and estimate undecidable problems. U PPAAL - SMC comes together with a friendly userinterface that allows a user to specify complex problems in an efficient manner as well as to getfeedback in the form of probability distributions and compare probabilities to analyze performanceaspects of systems. The focus of the survey is on the evolution of the tool – including modeling andspecification formalisms as well as techniques applied – together with applications of the tool to casestudies.

U2 - 10.4204/EPTCS.85.1

DO - 10.4204/EPTCS.85.1

M3 - Conference article in Journal

SN - 2075-2180

VL - 85

SP - 1

EP - 16

JO - Electronic Proceedings in Theoretical Computer Science

JF - Electronic Proceedings in Theoretical Computer Science

T2 - 10th Workshop on Quantitative Aspects of Programming Languages and Systems

Y2 - 31 March 2012 through 1 April 2012

ER -

UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata

Abstract

Conference

Access to Document

AUB Link

Fingerprint

Cite this