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

Bounded Retransmission in iUML-B State Machine: a Case Study

Han Peng, Chenglie Du, Haobin Wang

Abstract— This paper presents a case study using the iUML-B state machine to model bounded retransmission protocol. The case is inspired by Abrial's treatment of this example to illustrate the practicality of modeling control flow using the iUML-B state machine. The case study contains several aspects of our approach: (1) divide the system model into component state machines and control flow state machines; (2) modeling different types of variables using the state machine; (3) refinement method based on iUML-B state machine.

Index Terms— Event-B, control flow modelling, iUML-B state machine, bounded retransmission protocol

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, "Bounded Retransmission in iUML-B State Machine: a Case Study," Proceedings of 2017 the 7th International Workshop on Computer Science and Engineering, pp. 1144-1149, Beijing, 25-27 June, 2017.