%0 Conference Paper %1 jansen02 %A Jansen, David N. %A Hermanns, Holger %A Katoen, Joost-Pieter %B Intl. Symp. on Formal Techniques in Real-Time and Fault-Tolerant Systems %D 2002 %I Springer %K formal uml probabilistic %P 355--374 %T A Probabilistic Extension of UML Statecharts: Specification and Verification %U http://www.springerlink.com/(1s552trl0t3knz45nx1agt55)/app/home/contribution.asp?referrer=parent&backto=searcharticlesresults,1,5; %X This paper introduces means to specify system randomness within UML statecharts, and to verify probabilistic temporal properties over such enhanced statecharts which we call probabilistic UML statecharts. To achieve this, we develop a general recipe to extend a statechart semantics with discrete probability distributions, resulting in Markov decision processes as semantic models. We apply this recipe to the requirements-level UML semantics of 8. Properties of interest for probabilistic statecharts are expressed in PCTL, a probabilistic variant of CTL for processes that exhibit both non-determinism and probabilities. Verification is performed using the model checker PRISM. A model checking example shows the feasibility of the suggested approach.

@inproceedings{jansen02, abstract = {This paper introduces means to specify system randomness within UML statecharts, and to verify probabilistic temporal properties over such enhanced statecharts which we call probabilistic UML statecharts. To achieve this, we develop a general recipe to extend a statechart semantics with discrete probability distributions, resulting in Markov decision processes as semantic models. We apply this recipe to the requirements-level UML semantics of [8]. Properties of interest for probabilistic statecharts are expressed in PCTL, a probabilistic variant of CTL for processes that exhibit both non-determinism and probabilities. Verification is performed using the model checker PRISM. A model checking example shows the feasibility of the suggested approach.}, added-at = {2006-03-24T16:34:33.000+0100}, author = {Jansen, David N. and Hermanns, Holger and Katoen, Joost-Pieter}, biburl = {https://www.bibsonomy.org/bibtex/279eb5fe5f86964af11866685298beaeb/neilernst}, booktitle = {Intl. Symp. on Formal Techniques in Real-Time and Fault-Tolerant Systems}, citeulike-article-id = {494334}, description = {sdasda}, interhash = {a1fecd3c1d4a3cf6cf9ab46be9b2afc8}, intrahash = {79eb5fe5f86964af11866685298beaeb}, keywords = {formal uml probabilistic}, month = {September}, pages = {355--374}, priority = {0}, publisher = {Springer}, series = {LNCS 2469}, timestamp = {2006-03-24T16:34:33.000+0100}, title = {A Probabilistic Extension of UML Statecharts: Specification and Verification}, url = {http://www.springerlink.com/(1s552trl0t3knz45nx1agt55)/app/home/contribution.asp?referrer=parent\&backto=searcharticlesresults,1,5;}, year = 2002 }