Probabilistic UML statecharts for specification and verification: a case study

D.N. Jansen; J. Jürjens; M.V. Cengarle; E.B. Fernandez; B. Rumpe; R. Sander

Probabilistic UML statecharts for specification and verification: a case study

D.N. Jansen, J. Jürjens (Editor), M.V. Cengarle (Editor), E.B. Fernandez (Editor), B. Rumpe (Editor), R. Sander (Editor)

Research output: Contribution to conference › Paper › peer-review

Abstract

This paper introduces a probabilistic extension of UML statecharts. A requirements-level semantics of statecharts is extended to include probabilistic elements. Desired properties for probabilistic statecharts are expressed in the probabilistic logic PCTL, and verified using the model checker Prism. The extension simplifies the verification of critical systems with probabilistic elements, e. g. fault-tolerant systems. The extension is illustrated using a case study: a gambling machine. The theory behind this extension is explained in detail in a paper published recently [JHK02]; this article concentrates on the case study.

Original language	Undefined
Pages	121-131
Number of pages	11
Publication status	Published - 2002
Event	Critical systems development with UML: proceedings of the UML'02 workshop - Leipzig, Germany Duration: 1 Jan 2002 → 1 Jan 2002

Workshop

Workshop	Critical systems development with UML: proceedings of the UML'02 workshop
Period	1/01/02 → 1/01/02

Keywords

IR-62368
EWI-1295

Access to Document

Cite this

@conference{ddfe8d34be79416ea8472a744a756f3d,

title = "Probabilistic UML statecharts for specification and verification: a case study",

abstract = "This paper introduces a probabilistic extension of UML statecharts. A requirements-level semantics of statecharts is extended to include probabilistic elements. Desired properties for probabilistic statecharts are expressed in the probabilistic logic PCTL, and verified using the model checker Prism. The extension simplifies the verification of critical systems with probabilistic elements, e. g. fault-tolerant systems. The extension is illustrated using a case study: a gambling machine. The theory behind this extension is explained in detail in a paper published recently [JHK02]; this article concentrates on the case study.",

keywords = "IR-62368, EWI-1295",

author = "D.N. Jansen and J. J{\"u}rjens and M.V. Cengarle and E.B. Fernandez and B. Rumpe and R. Sander",

year = "2002",

language = "Undefined",

pages = "121--131",

note = "Critical systems development with UML: proceedings of the UML'02 workshop ; Conference date: 01-01-2002 Through 01-01-2002",

}

Jansen, DN, Jürjens, J (ed.), Cengarle, MV (ed.), Fernandez, EB (ed.), Rumpe, B (ed.) & Sander, R (ed.) 2002, 'Probabilistic UML statecharts for specification and verification: a case study', Paper presented at Critical systems development with UML: proceedings of the UML'02 workshop, 1/01/02 - 1/01/02 pp. 121-131. <http://eprints.eemcs.utwente.nl/secure2/1295/01/25.pdf>

TY - CONF

T1 - Probabilistic UML statecharts for specification and verification: a case study

AU - Jansen, D.N.

A2 - Jürjens, J.

A2 - Cengarle, M.V.

A2 - Fernandez, E.B.

A2 - Rumpe, B.

A2 - Sander, R.

PY - 2002

Y1 - 2002

N2 - This paper introduces a probabilistic extension of UML statecharts. A requirements-level semantics of statecharts is extended to include probabilistic elements. Desired properties for probabilistic statecharts are expressed in the probabilistic logic PCTL, and verified using the model checker Prism. The extension simplifies the verification of critical systems with probabilistic elements, e. g. fault-tolerant systems. The extension is illustrated using a case study: a gambling machine. The theory behind this extension is explained in detail in a paper published recently [JHK02]; this article concentrates on the case study.

AB - This paper introduces a probabilistic extension of UML statecharts. A requirements-level semantics of statecharts is extended to include probabilistic elements. Desired properties for probabilistic statecharts are expressed in the probabilistic logic PCTL, and verified using the model checker Prism. The extension simplifies the verification of critical systems with probabilistic elements, e. g. fault-tolerant systems. The extension is illustrated using a case study: a gambling machine. The theory behind this extension is explained in detail in a paper published recently [JHK02]; this article concentrates on the case study.

KW - IR-62368

KW - EWI-1295

M3 - Paper

SP - 121

EP - 131

T2 - Critical systems development with UML: proceedings of the UML'02 workshop

Y2 - 1 January 2002 through 1 January 2002

ER -