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


Han Peng, Chenglie Du, Lei Rao, Zhouzhou Liu, Journal of Information Processing Systems
Vol. 15, No. 3, pp. 570-592, Jun. 2019
10.3745/JIPS.01.0043
Keywords: Behavior Semantic, Design Pattern Instantiation, Event-B Design Patterns, Labeled Transition System
Fulltext:

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.


Statistics
Show / Hide Statistics

Statistics (Cumulative Counts from November 1st, 2017)
Multiple requests among the same browser session are counted as one view.
If you mouse over a chart, the values of data points will be shown.




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

[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.