Probabilistic UML statecharts for specification and verification: a case study

D.N. Jansen, J. Jürjens (Editor), M.V. Cengarle (Editor), E.B. Fernandez (Editor), B. Rumpe (Editor), R. Sander (Editor)

    Research output: Contribution to conferencePaper

    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.
    Original languageUndefined
    Pages121-131
    Number of pages11
    Publication statusPublished - 2002

    Keywords

    • IR-62368
    • EWI-1295

    Cite this

    Jansen, D. N., Jürjens, J. (Ed.), Cengarle, M. V. (Ed.), Fernandez, E. B. (Ed.), Rumpe, B. (Ed.), & Sander, R. (Ed.) (2002). Probabilistic UML statecharts for specification and verification: a case study. 121-131.