文章基本信息

标题：Preservation of Dynamic Behaviours in a Hierarchical Event Structure
本地全文：下载
作者：Weidong Tang ; Jinzhao Wu
期刊名称：Journal of Software
印刷版ISSN：1796-217X
出版年度：2016
卷号：11
期号：8
页码：712-732
DOI：10.17706/jsw.11.8.712-732
出版社：Academy Publisher
摘要：Event structure is a method of modelling and verification for concurrent system, and action refinement is the core operation in event structure. This paper researches on what conditions action refinement must satisfy, such that some structural properties and dynamic properties of contour model, such as connectivity, liveness, fairness and regression, can also be preserved in its detailed model. In researching on the dynamic properties of event structure, it is difficult to apply event structure model to represent infinite events, this is because each action can be executed infinite times, thus it will produce infinite events. There has been little research on the problem. Therefore, we propose the concept of action structure model. The differences between the action structure model and event structure model include: (1)The events in event structure model are replaced by actions, and the same actions are merged into one action; (2) The inheritance of causality and the inheritance of conflict relation are no longer preserved; (3) When an action is executed even times, it will not appear in the configuration; and when an action is executed odd times, it will appear in the configuration. The use of action structure model can easily solve the difficult problem of representation of infinite events which encountered in the event structure model. This paper gives an example to demonstrate the application of action structure model.
其他关键词：Action structure model, action refinement, reachability, dynamic behaviour