A Probabilistic Extension of UML-B

Year, pages: 2019, 85 - 114

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.

Nosrati, M., Haghighi, H. 2019. A Probabilistic Extension of UML-B. In Computing and Informatics, vol. 38, no.1, pp. 85-114. 1335-9150. DOI: https://doi.org/10.31577/cai_2019_1_85

Nosrati, M., Haghighi, H. (2019). A Probabilistic Extension of UML-B. Computing and Informatics, 38(1), 85-114. 1335-9150. DOI: https://doi.org/10.31577/cai_2019_1_85

Publisher: Ústav informatiky SAV