A probabilistic extension of UML statecharts: Specification and Verification.

Jansen, David N. and Hermanns, Holger and Katoen, Joost-Pieter (2002) A probabilistic extension of UML statecharts: Specification and Verification. In: 7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2002, September 9-12, 2002, Oldenburg, Germany.

PDF
Restricted to UT campus only: Request a copy
294Kb

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.
Item Type:	Conference or Workshop Item
Copyright:	© 2002 Springer
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Formal Methods and Tools (FMT)
Link to this item:	http://purl.utwente.nl/publications/38587
Official URL:	http://dx.doi.org/10.1007/3-540-45739-9
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page

Metis ID: 211963