A probabilistic extension of UML statecharts: specification and verification

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

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

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 languageUndefined
Title of host publicationFormal techniques in real-time and fault-tolerant systems: ... FTRTFT
EditorsW. Damm, E.-R. Olderog
Place of PublicationBerlin, Germany
PublisherSpringer
Pages355-374
Number of pages20
ISBN (Print)3-540-44165-4
DOIs
Publication statusPublished - 2002
Event7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2002 - Oldenburg, Germany
Duration: 9 Sep 200212 Sep 2002
Conference number: 7

Publication series

NameLecture Notes in Computer Science
PublisherSpringer-Verlag
Volume2469
ISSN (Print)0302-9743

Conference

Conference7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2002
Abbreviated titleFTRTFT
CountryGermany
CityOldenburg
Period9/09/0212/09/02

Keywords

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

Cite this

Jansen, D. N., Hermanns, H., & Katoen, J. P. (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 (pp. 355-374). (Lecture Notes in Computer Science; Vol. 2469). Berlin, Germany: Springer. https://doi.org/10.1007/3-540-45739-9
Jansen, D.N. ; Hermanns, H. ; Katoen, Joost P. / A probabilistic extension of UML statecharts: specification and verification. Formal techniques in real-time and fault-tolerant systems: ... FTRTFT. editor / W. Damm ; E.-R. Olderog. Berlin, Germany : Springer, 2002. pp. 355-374 (Lecture Notes in Computer Science).
@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",
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",

}

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 proceedingConference contributionAcademicpeer-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 - LNCS-2469

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

ER -

Jansen DN, Hermanns H, Katoen JP. A probabilistic extension of UML statecharts: specification and verification. In Damm W, Olderog E-R, editors, Formal techniques in real-time and fault-tolerant systems: ... FTRTFT. Berlin, Germany: Springer. 2002. p. 355-374. (Lecture Notes in Computer Science). https://doi.org/10.1007/3-540-45739-9