A probabilistic extension of UML statecharts: specification and verification

D.N. Jansen, H. Hermanns, Joost P. Katoen

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    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.
    Original languageUndefined
    Title of host publicationFormal techniques in real-time and fault-tolerant systems: ... FTRTFT
    EditorsW. Damm, E.-R. Olderog
    Place of PublicationBerlin, Germany
    PublisherSpringer
    Pages355-374
    Number of pages20
    ISBN (Print)3-540-44165-4
    DOIs
    Publication statusPublished - 2002
    Event7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2002 - Oldenburg, Germany
    Duration: 9 Sep 200212 Sep 2002
    Conference number: 7

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer-Verlag
    Volume2469
    ISSN (Print)0302-9743

    Conference

    Conference7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2002
    Abbreviated titleFTRTFT
    CountryGermany
    CityOldenburg
    Period9/09/0212/09/02

    Keywords

    • EWI-1299
    • UML statecharts
    • probabilities
    • Semantics
    • IR-38587
    • Model Checking
    • Markov Decision Processes
    • METIS-211963

    Cite this

    Jansen, D. N., Hermanns, H., & Katoen, J. P. (2002). A probabilistic extension of UML statecharts: specification and verification. In W. Damm, & E-R. Olderog (Eds.), Formal techniques in real-time and fault-tolerant systems: ... FTRTFT (pp. 355-374). (Lecture Notes in Computer Science; Vol. 2469). Berlin, Germany: Springer. https://doi.org/10.1007/3-540-45739-9
    Jansen, D.N. ; Hermanns, H. ; Katoen, Joost P. / A probabilistic extension of UML statecharts: specification and verification. Formal techniques in real-time and fault-tolerant systems: ... FTRTFT. editor / W. Damm ; E.-R. Olderog. Berlin, Germany : Springer, 2002. pp. 355-374 (Lecture Notes in Computer Science).
    @inproceedings{f0953a3e9b8942ddb855f493ea806e11,
    title = "A probabilistic extension of UML statecharts: specification and verification",
    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.",
    keywords = "EWI-1299, UML statecharts, probabilities, Semantics, IR-38587, Model Checking, Markov Decision Processes, METIS-211963",
    author = "D.N. Jansen and H. Hermanns and Katoen, {Joost P.}",
    note = "LNCS-2469",
    year = "2002",
    doi = "10.1007/3-540-45739-9",
    language = "Undefined",
    isbn = "3-540-44165-4",
    series = "Lecture Notes in Computer Science",
    publisher = "Springer",
    pages = "355--374",
    editor = "W. Damm and E.-R. Olderog",
    booktitle = "Formal techniques in real-time and fault-tolerant systems: ... FTRTFT",

    }

    Jansen, DN, Hermanns, H & Katoen, JP 2002, A probabilistic extension of UML statecharts: specification and verification. in W Damm & E-R Olderog (eds), Formal techniques in real-time and fault-tolerant systems: ... FTRTFT. Lecture Notes in Computer Science, vol. 2469, Springer, Berlin, Germany, pp. 355-374, 7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2002, Oldenburg, Germany, 9/09/02. https://doi.org/10.1007/3-540-45739-9

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

    Formal techniques in real-time and fault-tolerant systems: ... FTRTFT. ed. / W. Damm; E.-R. Olderog. Berlin, Germany : Springer, 2002. p. 355-374 (Lecture Notes in Computer Science; Vol. 2469).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    TY - GEN

    T1 - A probabilistic extension of UML statecharts: specification and verification

    AU - Jansen, D.N.

    AU - Hermanns, H.

    AU - Katoen, Joost P.

    N1 - LNCS-2469

    PY - 2002

    Y1 - 2002

    N2 - 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.

    AB - 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.

    KW - EWI-1299

    KW - UML statecharts

    KW - probabilities

    KW - Semantics

    KW - IR-38587

    KW - Model Checking

    KW - Markov Decision Processes

    KW - METIS-211963

    U2 - 10.1007/3-540-45739-9

    DO - 10.1007/3-540-45739-9

    M3 - Conference contribution

    SN - 3-540-44165-4

    T3 - Lecture Notes in Computer Science

    SP - 355

    EP - 374

    BT - Formal techniques in real-time and fault-tolerant systems: ... FTRTFT

    A2 - Damm, W.

    A2 - Olderog, E.-R.

    PB - Springer

    CY - Berlin, Germany

    ER -

    Jansen DN, Hermanns H, Katoen JP. A probabilistic extension of UML statecharts: specification and verification. In Damm W, Olderog E-R, editors, Formal techniques in real-time and fault-tolerant systems: ... FTRTFT. Berlin, Germany: Springer. 2002. p. 355-374. (Lecture Notes in Computer Science). https://doi.org/10.1007/3-540-45739-9