A probabilistic extension of UML statecharts: specification and verification

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

Research output: Book/ReportReport

  • 29 Citations

Abstract

This paper is the extended technical report that corresponds to a published paper [14]. 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.
LanguageUndefined
Place of PublicationEnschede
PublisherCentre for Telematics and Information Technology (CTIT)
Number of pages25
StatePublished - Sep 2002

Publication series

NameCTIT technical report series
PublisherUniversity of Twente, Centre for Telematics and Information Technology (CTIT)
No.TR-CTIT-02-31

Keywords

  • UML statecharts
  • Model Checking
  • EWI-1300
  • Semantics
  • IR-56024
  • probabilities
  • Markov Decision Processes

Cite this

Jansen, D. N., Hermanns, H., & Katoen, J. P. (2002). A probabilistic extension of UML statecharts: specification and verification. (CTIT technical report series; No. TR-CTIT-02-31). Enschede: Centre for Telematics and Information Technology (CTIT).
Jansen, D.N. ; Hermanns, H. ; Katoen, Joost P./ A probabilistic extension of UML statecharts: specification and verification. Enschede : Centre for Telematics and Information Technology (CTIT), 2002. 25 p. (CTIT technical report series; TR-CTIT-02-31).
@book{e7d2fe57e9ed48488fe700aff406b11e,
title = "A probabilistic extension of UML statecharts: specification and verification",
abstract = "This paper is the extended technical report that corresponds to a published paper [14]. 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 = "UML statecharts, Model Checking, EWI-1300, Semantics, IR-56024, probabilities, Markov Decision Processes",
author = "D.N. Jansen and H. Hermanns and Katoen, {Joost P.}",
year = "2002",
month = "9",
language = "Undefined",
series = "CTIT technical report series",
publisher = "Centre for Telematics and Information Technology (CTIT)",
number = "TR-CTIT-02-31",
address = "Netherlands",

}

Jansen, DN, Hermanns, H & Katoen, JP 2002, A probabilistic extension of UML statecharts: specification and verification. CTIT technical report series, no. TR-CTIT-02-31, Centre for Telematics and Information Technology (CTIT), Enschede.

A probabilistic extension of UML statecharts: specification and verification. / Jansen, D.N.; Hermanns, H.; Katoen, Joost P.

Enschede : Centre for Telematics and Information Technology (CTIT), 2002. 25 p. (CTIT technical report series; No. TR-CTIT-02-31).

Research output: Book/ReportReport

TY - BOOK

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

AU - Jansen,D.N.

AU - Hermanns,H.

AU - Katoen,Joost P.

PY - 2002/9

Y1 - 2002/9

N2 - This paper is the extended technical report that corresponds to a published paper [14]. 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 is the extended technical report that corresponds to a published paper [14]. 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 - UML statecharts

KW - Model Checking

KW - EWI-1300

KW - Semantics

KW - IR-56024

KW - probabilities

KW - Markov Decision Processes

M3 - Report

T3 - CTIT technical report series

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

PB - Centre for Telematics and Information Technology (CTIT)

CY - Enschede

ER -

Jansen DN, Hermanns H, Katoen JP. A probabilistic extension of UML statecharts: specification and verification. Enschede: Centre for Telematics and Information Technology (CTIT), 2002. 25 p. (CTIT technical report series; TR-CTIT-02-31).