Event-B Control Flow Modeling based on iUML-B State Machine

There are some limitations in expressing the order of actions using Event-B. To solve this problem, the event refinement structure method (ERS) is proposed to facilitate modeling of the system’s control flow. However, the event refinement structure cannot be translated to a behavior semantic model such as the communication sequence process (CSP) or labeled transition system (LTS) directly, thus it is not convenient for engineers to verify the control flow. In this paper, we first propose a general method to model the control flow of the Event-B model with various iUML-B state machines. Then we prove by simulation that the event trace of the iUML-B state machine is the same as that of the event refinement structure method. Finally, we use a case study of a lift control system to prove the practicality of our method.

@article{Peng2018,
  title     = {Event-B Control Flow Modeling based on iUML-B State Machine},
  journal   = {International Journal of Advanced Computer Science and Applications},
  volume    = {9},
  number    = {1},
  year      = {2018},
  publisher = {The Science and Information Organization},
  author    = {Han Peng and Chenglie Du and Haobin Wang},
  doi       = {10.14569/SpecialIssue.2018.090153},
  url       = {https://doi.org/10.14569/SpecialIssue.2018.090153}
}