A Probabilistic Extension of UML-B
Keywords:UML-B, Event-B, probabilistic systems, interval probabilities, stochastic delay, probabilistic model verification, MDP, PRISM
AbstractThis 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