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