A probabilistic extension of UML statecharts: Specification and Verification.

摘要: This paper introduces means to specify system randomness within UML statecharts, and verify probabilistic temporal properties over such enhanced statecharts which we call statecharts. To achieve this, develop a general recipe extend statechart semantics with discrete probability distributions, resulting in Markov decision processes as semantic models. We apply this the requirements-level of [8]. Properties interest for are expressed PCTL, variant CTL that exhibit both non-determinism probabilities. Verification is performed using model checker PRISM. A checking example shows feasibility suggested approach.