A Probabilistic Extension of UML Statecharts
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 . 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.
KeywordsMarkov decision processes model checking probabilities semantics UML statecharts
- 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.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.Philip H. Crowley. Hawks, doves, and mixed-symmetry games. Journal of Theoretical Biology, 204(4):543–563, June 2000.Google Scholar
- 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.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.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: http://www.elsevier.nl/locate/entcs/volume22.html.
- 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.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.H. A. Hansson. Time and Probability in Formal Design of Distributed Systems. PhD thesis, University of Uppsala, 1991.Google Scholar
- 12.David Harel and Eran Gery. Executable object modeling with statecharts. Computer, 30(7):31–42, July 1997. IEEE.Google Scholar
- 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.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.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.J. Maynard Smith and G. R. Price. The logic of animal conflict. Nature, 246, November 1973.Google Scholar
- 18.S. McMenamin and J. Palmer. Essential Systems Analysis. Yourdon Press, New York, 1984.Google Scholar
- 21.A. N. Shiryaev. Probability, volume 95 of Graduate texts in mathematics. Springer, New York, 1996.Google Scholar
- 22.UML Revision Task Force. OMG UML Specification 1.3. Object Management Group, 1999. http://www.omg.org/cgi-bin/doc?ad/99-06-08.