A Probabilistic Extension of UML-B


  • Mohammad Nosrati Shahid Beheshti University, Evin, Tehran, Iran
  • Hassan Haghighi Shahid Beheshti University, Evin, Tehran, Iran




UML-B, Event-B, probabilistic systems, interval probabilities, stochastic delay, probabilistic model verification, MDP, PRISM


This paper extends the graphical and formal language of UML-B to provide the ability to model probabilities. Discrete probabilities, interval probabilities, and stochastic delays are added to the UML-B's state-machine syntax, and their corresponding semantics are defined in Event-B. In addition, as a secondary contribution, UML-B (probabilistic) state-machine models are defined as MDP (Markov Decision Process) models in order to provide a means of quantitative verification in PRISM (Probabilistic Symbolic Model Checker). As an important feature of the proposed method, it does not change the Event-B syntax or semantics. To evaluate this work, as a case study, the Zeroconf protocol will be modeled in the extended UML-B using the Rodin tool, and its Event-B counterpart is converted to a PRISM model. The results of evaluations indicate that this study's additions provide the capability of modeling and verification of probabilistic and stochastic systems.


Download data is not yet available.




How to Cite

Nosrati, M., & Haghighi, H. (2019). A Probabilistic Extension of UML-B. COMPUTING AND INFORMATICS, 38(1), 85–114. https://doi.org/10.31577/cai_2019_1_85

Most read articles by the same author(s)