WCSE 2017
ISBN: 978-981-11-3671-9 DOI: 10.18178/wcse.2017.06.206

Modeling Control Flow of Event-B Using State Transition System

Han Peng, Chenglie Du, Haobin Wang

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.