A probabilistic extension of UML statecharts: specification and verification

D.N. Jansen; H. Hermanns; Joost P. Katoen

doi:10.1007/3-540-45739-9

A probabilistic extension of UML statecharts: specification and verification

D.N. Jansen, H. Hermanns, Joost P. Katoen

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

1 Downloads (Pure)

Abstract

This paper introduces means to specify system randomness within UML statecharts, and to verify probabilistic temporal properties over such enhanced statecharts which we call probabilistic UML statecharts. To achieve this, we develop a general recipe to extend a statechart semantics with discrete probability distributions, resulting in Markov decision processes as semantic models. We apply this recipe to the requirements-level UML semantics of [8]. Properties of interest for probabilistic statecharts are expressed in PCTL, a probabilistic variant of CTL for processes that exhibit both non-determinism and probabilities. Verification is performed using the model checker PRISM. A model checking example shows the feasibility of the suggested approach.

Original language	Undefined
Title of host publication	Formal techniques in real-time and fault-tolerant systems: ... FTRTFT
Editors	W. Damm, E.-R. Olderog
Place of Publication	Berlin, Germany
Publisher	Springer
Pages	355-374
Number of pages	20
ISBN (Print)	3-540-44165-4
DOIs	https://doi.org/10.1007/3-540-45739-9
Publication status	Published - 2002
Event	7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2002 - Oldenburg, Germany Duration: 9 Sept 2002 → 12 Sept 2002 Conference number: 7

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer-Verlag
Volume	2469
ISSN (Print)	0302-9743

Conference

Conference	7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2002
Abbreviated title	FTRTFT
Country/Territory	Germany
City	Oldenburg
Period	9/09/02 → 12/09/02

Keywords

EWI-1299
UML statecharts
probabilities
Semantics
IR-38587
Model Checking
Markov Decision Processes
METIS-211963

Access to Document

10.1007/3-540-45739-9

http://eprints.eemcs.utwente.nl/secure2/1299/01/jcf7jmnfbvgvd0wx.pdf

Cite this

@inproceedings{f0953a3e9b8942ddb855f493ea806e11,

title = "A probabilistic extension of UML statecharts: specification and verification",

abstract = "This paper introduces means to specify system randomness within UML statecharts, and to verify probabilistic temporal properties over such enhanced statecharts which we call probabilistic UML statecharts. To achieve this, we develop a general recipe to extend a statechart semantics with discrete probability distributions, resulting in Markov decision processes as semantic models. We apply this recipe to the requirements-level UML semantics of [8]. Properties of interest for probabilistic statecharts are expressed in PCTL, a probabilistic variant of CTL for processes that exhibit both non-determinism and probabilities. Verification is performed using the model checker PRISM. A model checking example shows the feasibility of the suggested approach.",

keywords = "EWI-1299, UML statecharts, probabilities, Semantics, IR-38587, Model Checking, Markov Decision Processes, METIS-211963",

author = "D.N. Jansen and H. Hermanns and Katoen, {Joost P.}",

note = "LNCS-2469 ; 7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2002 ; Conference date: 09-09-2002 Through 12-09-2002",

year = "2002",

doi = "10.1007/3-540-45739-9",

language = "Undefined",

isbn = "3-540-44165-4",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "355--374",

editor = "W. Damm and E.-R. Olderog",

booktitle = "Formal techniques in real-time and fault-tolerant systems: ... FTRTFT",

address = "Germany",

}

Jansen, DN, Hermanns, H & Katoen, JP 2002, A probabilistic extension of UML statecharts: specification and verification. in W Damm & E-R Olderog (eds), Formal techniques in real-time and fault-tolerant systems: ... FTRTFT. Lecture Notes in Computer Science, vol. 2469, Springer, Berlin, Germany, pp. 355-374, 7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2002, Oldenburg, Germany, 9/09/02. https://doi.org/10.1007/3-540-45739-9

A probabilistic extension of UML statecharts: specification and verification. / Jansen, D.N.; Hermanns, H.; Katoen, Joost P.
Formal techniques in real-time and fault-tolerant systems: ... FTRTFT. ed. / W. Damm; E.-R. Olderog. Berlin, Germany: Springer, 2002. p. 355-374 (Lecture Notes in Computer Science; Vol. 2469).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - A probabilistic extension of UML statecharts: specification and verification

AU - Jansen, D.N.

AU - Hermanns, H.

AU - Katoen, Joost P.

N1 - Conference code: 7

PY - 2002

Y1 - 2002

N2 - This paper introduces means to specify system randomness within UML statecharts, and to verify probabilistic temporal properties over such enhanced statecharts which we call probabilistic UML statecharts. To achieve this, we develop a general recipe to extend a statechart semantics with discrete probability distributions, resulting in Markov decision processes as semantic models. We apply this recipe to the requirements-level UML semantics of [8]. Properties of interest for probabilistic statecharts are expressed in PCTL, a probabilistic variant of CTL for processes that exhibit both non-determinism and probabilities. Verification is performed using the model checker PRISM. A model checking example shows the feasibility of the suggested approach.

AB - This paper introduces means to specify system randomness within UML statecharts, and to verify probabilistic temporal properties over such enhanced statecharts which we call probabilistic UML statecharts. To achieve this, we develop a general recipe to extend a statechart semantics with discrete probability distributions, resulting in Markov decision processes as semantic models. We apply this recipe to the requirements-level UML semantics of [8]. Properties of interest for probabilistic statecharts are expressed in PCTL, a probabilistic variant of CTL for processes that exhibit both non-determinism and probabilities. Verification is performed using the model checker PRISM. A model checking example shows the feasibility of the suggested approach.

KW - EWI-1299

KW - UML statecharts

KW - probabilities

KW - Semantics

KW - IR-38587

KW - Model Checking

KW - Markov Decision Processes

KW - METIS-211963

U2 - 10.1007/3-540-45739-9

DO - 10.1007/3-540-45739-9

M3 - Conference contribution

SN - 3-540-44165-4

T3 - Lecture Notes in Computer Science

SP - 355

EP - 374

BT - Formal techniques in real-time and fault-tolerant systems: ... FTRTFT

A2 - Damm, W.

A2 - Olderog, E.-R.

PB - Springer

CY - Berlin, Germany

T2 - 7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2002

Y2 - 9 September 2002 through 12 September 2002

ER -