A Probabilistic Extension of UML Statecharts

Specification and Verification
  • David N. Jansen
  • Holger Hermanns
  • Joost-Pieter Katoen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2469)


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.


Markov decision processes model checking probabilities semantics UML statecharts 


  1. 1.
    Christel Baier and Marta Kwiatkowska. Model checking for a probabilistic branching time logic with fairness. Distributed Computing, 11(3):125–155, 1998.CrossRefGoogle Scholar
  2. 2.
    Michael von der Beeck. A comparison of statecharts variants. In H. Langmaack, W.-P. de Roever, and J. Vytopil, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems:...proceedings, pages 128–148, Berlin, 1994. Springer.Google Scholar
  3. 3.
    Andrea Bianco and Luca de Alfaro. Model checking of probabilistic and nondeter-ministic systems. In P. S. Thiagarajan, editor, Foundations of Software Technology and Theoretical Computer Science:... proceedings, volume 1026 of LNCS, pages 499–513, Berlin, 1995. Springer.Google Scholar
  4. 4.
    Philip H. Crowley. Hawks, doves, and mixed-symmetry games. Journal of Theoretical Biology, 204(4):543–563, June 2000.Google Scholar
  5. 5.
    M. Dal Cin, G. Huszerl, and K. Kosmidis. Evaluation of dependability critical systems based on guarded statechart models. In 4th Int. Symp. on High Assurance Systems Engineering (HASE), pages 37–45. IEEE, 1999.Google Scholar
  6. 6.
    Werner Damm, Bernhard Josko, Hardi Hungar, and Amir Pnueli. A compositional real-time semantics of statemate designs. In Willem-Paul de Roever, Hans Langmaack, and Amir Pnueli, editors, Compositionality: the significant difference. COMPOS’ 97, volume 1536 of LNCS, pages 186–238, Berlin, 1998. Springer.CrossRefGoogle Scholar
  7. 7.
    Pedro R. D’Argenio, Holger Hermanns, and Joost-Pieter Katoen. On generative parallel composition. In Christel Baier, Michael Huth, Marta Kwiatkowska, and Mark Ryan, editors, PROBMIV’98 First International Workshop on Probabilistic Methods in Verification: Indianapolis, Ind.... 1998, volume 22 of Electronic Notes in Theoretical Computer Science. Elsevier, 2000. URL:
  8. 8.
    Rik Eshuis and Roel Wieringa. Requirements-level semantics for UML statecharts. In Scott F. Smith and Carolyn L. Talcott, editors, Formal Methods for Open Object-Based Distributed Systems IV:... FMOODS, pages 121–140, Boston, 2000. Kluwer Academic Publishers.Google Scholar
  9. 9.
    Stefania Gnesi, Diego Latella, and Mieke Massink. A stochastic extension of a behavioural subset of UML statechart diagrams. In L. Palagi and R. Bilof, editors, Fifth International Symposium on High-Assurance Systems Engineering (HASE), pages 55–64. IEEE Computer Society Press, 2000.Google Scholar
  10. 10.
    H. A. Hansson. Time and Probability in Formal Design of Distributed Systems. PhD thesis, University of Uppsala, 1991.Google Scholar
  11. 11.
    Hans Hansson and Bengt Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6:512–535, 1994.zbMATHCrossRefGoogle Scholar
  12. 12.
    David Harel and Eran Gery. Executable object modeling with statecharts. Computer, 30(7):31–42, July 1997. IEEE.Google Scholar
  13. 13.
    David Harel and Amnon Naamad. The STATEMATE semantics of statecharts. ACM Transactions on Software Engineering and Methodology, 5(4):293–333, 1996.CrossRefGoogle Scholar
  14. 14.
    Peter King and Rob Pooley. Derivation of Petri net performance models from UML specifications of communications software. In Boudewijn R. Haverkort, Henrik C. Bohnenkamp, and Connie U. Smith, editors, Computer Performance Evaluation: Modelling Techniques and Tools;... TOOLS 2000, volume 1786 of LNCS, pages 262–276, Berlin, 2000. Springer.CrossRefGoogle Scholar
  15. 15.
    Marta Kwiatkowska, Gethin Norman, and David Parker. Probabilistic symbolic model checking with prism: A hybrid approach. In Joost-Pieter Katoen and Perdita Stevens, editors, Tools and Algorithms for the Construction and Analysis of Algorithms:.. TACAS, volume 2280 of LNCS, pages 52–66, Berlin, 2002. Springer.CrossRefGoogle Scholar
  16. 16.
    C. Lindemann, A. Thümmler, A. Klemm, M. Lohmann, and O. P. Waldhorst. Quantitative system evaluation with DSPNexpress 2000. In Workshop on Software and Performance (WOSP), pages 12–17. ACM, 2000.Google Scholar
  17. 17.
    J. Maynard Smith and G. R. Price. The logic of animal conflict. Nature, 246, November 1973.Google Scholar
  18. 18.
    S. McMenamin and J. Palmer. Essential Systems Analysis. Yourdon Press, New York, 1984.Google Scholar
  19. 19.
    Martin L. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, New York, 1994.zbMATHGoogle Scholar
  20. 20.
    R. Segala and N. Lynch. Probabilistic simulations for probabilistic processes. Nordic Journal of Computing, 2:250–273, 1995.zbMATHMathSciNetGoogle Scholar
  21. 21.
    A. N. Shiryaev. Probability, volume 95 of Graduate texts in mathematics. Springer, New York, 1996.Google Scholar
  22. 22.
    UML Revision Task Force. OMG UML Specification 1.3. Object Management Group, 1999.

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • David N. Jansen
    • 1
  • Holger Hermanns
    • 2
  • Joost-Pieter Katoen
    • 2
  1. 1.Information Systems GroupUniversiteit TwenteAE EnschedeThe Netherlands
  2. 2.Formal Methods and Tools GroupUniversiteit TwenteAE EnschedeThe Netherlands

Personalised recommendations