LTS Semantics Model of Event-B Synchronization Control Flow Design Patterns

Han Peng, Chenglie Du, Lei Rao and Zhouzhou Liu
Volume: 15, No: 3, Page: 570 ~ 592, Year: 2019
10.3745/JIPS.01.0043
Keywords: Behavior Semantic, Design Pattern Instantiation, Event-B Design Patterns, Labeled Transition System
Full Text:

Abstract
The Event-B design pattern is an excellent way to quickly develop a formal model of the system. Researchers have proposed a number of Event-B design patterns, but they all lack formal behavior semantics. This makes the analysis, verification, and simulation of the behavior of the Event-B model very difficult, especially for the control-intensive systems. In this paper, we propose a novel method to transform the Event-B synchronous control flow design pattern into the labeled transition system (LTS) behavior model. Then we map the design pattern instantiation process of Event-B to the instantiation process of LTS model and get the LTS behavior semantic model of Event-B model of a multi-level complex control system. Finally, we verify the linear temporal logic behavior properties of the LTS model. The experimental results show that the analysis and simulation of system behavior become easier and the verification of the behavior properties of the system become convenient after the Event-B model is converted to the LTS model.

Article Statistics
Multiple requests among the same broswer session are counted as one view (or download).
If you mouse over a chart, a box will show the data point's value.


Cite this article
IEEE Style
H. Peng, C. Du, L. Rao and Z. Liu, "LTS Semantics Model of Event-B Synchronization Control Flow Design Patterns," Journal of Information Processing Systems, vol. 15, no. 3, pp. 570~592, 2019. DOI: 10.3745/JIPS.01.0043.

ACM Style
Han Peng, Chenglie Du, Lei Rao, and Zhouzhou Liu. 2019. LTS Semantics Model of Event-B Synchronization Control Flow Design Patterns, Journal of Information Processing Systems, 15, 3, (2019), 570~592. DOI: 10.3745/JIPS.01.0043.