A Probabilistic Extension of UML-B

Mohammad Nosrati; Hassan Haghighi

doi:10.31577/cai_2019_1_85

Abstract

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.

Keywords

Cite this article

@article{cai-3993,
  author  = {Mohammad Nosrati and Hassan Haghighi},
  title   = {A Probabilistic Extension of UML-B},
  journal = {Computing and Informatics},
  volume  = {38},
  number  = {1},
  pages   = {85--114},
  year    = {2019},
  issn    = {1335-9150},
  doi     = {10.31577/cai_2019_1_85}
}

Download .bib

TY  - JOUR
AU  - Mohammad Nosrati
AU  - Hassan Haghighi
TI  - A Probabilistic Extension of UML-B
JO  - Computing and Informatics
VL  - 38
IS  - 1
SP  - 85
EP  - 114
PY  - 2019
SN  - 1335-9150
DO  - 10.31577/cai_2019_1_85
UR  - https://doi.org/10.31577/cai_2019_1_85
KW  - UML-B
KW  - Event-B
KW  - probabilistic systems
KW  - interval probabilities
KW  - stochastic delay
KW  - probabilistic model verification
KW  - MDP
KW  - PRISM
ER  -

Download .ris

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

Download .txt