文档介绍：Probabilistic UML Statecharts
for Specification and Verification
a case study
David N. Jansen
Universiteit Twente, Information Systems Group.
Postbus 217, 7500 AE Enschede, herlands.
******@
Abstract. This paper introduces a probabilistic extension of UML stat-
echarts. A requirements-level semantics of statecharts is extended to
include the probabilistic elements. Desired properties for probabilistic
statecharts are expressed in PCTL, and verified using the model checker
Prism. The extension is illustrated using a case study: a gambling ma-
chine.
The theory behind this extension is explained in detail in a paper pub-
lished recently [9]; this article concentrates on the case study.
1 Introduction
The UML hardly needs any justification at this conference. It is being used to
describe more systems, and an increasing number of engineers get used to it. I
believe that the UML will be used even in domains it was never designed for;
accordingly, it is not far fetched to predict that the following years shall see
substantial efforts to extend the UML towards soft real-time, fault-tolerance,
quality of service and the like. First work in this direction has been undertaken,
e. g., in [2, 5, 10, 12].
One of the principal modelling paradigms needed to express such aspects is
the concept of probability, allowing one to quantitatively descr