ISBN: 978-981-11-3671-9 DOI: 10.18178/wcse.2017.06.206
Modeling Control Flow of Event-B Using State Transition System
Abstract— There are some limitations of Event-B method in expressing the event order of system. In order
to solve this problem, event refinement structure method was proposed to model the system refinement
structure and control flow. However, the event refinement structure diagram cannot directly map to a
behavioral semantic model such as communication sequence process or labeled transition system, and is
inconvenient to verify the behavior properties of system. In this paper, we propose a general method to model
the control flow of the Event-B model with the iUML-B state machine; so that it has the same event traces as
the event refinement structure method. Then, we use a simple case to prove the practicality of this method.
Finally, we map the iUML-B state machine to a labeled transition system and verify the behavior properties
of the system.
Index Terms— Event-B, control flow modeling, labeled transition system, iUML-B state machine
Han Peng, Chenglie Du
College of Computer Science, Northwestern Polytechnical University, CHINA
Haobin Wang
College of Computer Science, Xi'an Aeronautical University, CHINA
ISBN: 978-981-11-3671-9 DOI: 10.18178/wcse.2017.06.17Xsrc="http://www.wcse.org/uploadfile/2019/0823/20190823055609629.png" style="width: 120px; height: 68px;" />[Download]
Cite: Han Peng, Chenglie Du, Haobin Wang, "Modeling Control Flow of Event-B Using State Transition System," Proceedings of 2017 the 7th International Workshop on Computer Science and Engineering, pp. 1179-1186, Beijing, 25-27 June, 2017.