Open Access Open Access  Restricted Access Subscription Access

Model-Based Data-Intensive Service Abstraction Refinement

Yu-Yu Yin,
Hong-Hao Gao,
Dong-Jin Yu,


As an important technique to encapsulate data and integrate computing resources over Internet, Web service becomes one of the most promising infrastructures for developing the cross-platform application in SOA and SOC. However, due to the characteristics of heterogeneous, open, and collaborative, the correctness of data-intensive service should be guaranteed during its application. Considering the explosive data among services, this paper proposes a model-based data-intensive services abstraction refinement to model and verify the data-intensive service. First, the data flows and service interactions are formalized into DEFSM (Data-Related Extended Finite State Machine) model, which can describe the functional interactions and their parallel interactions. Second, the CEGAR (Counterexample-Guided Abstraction Refinement) method is employed to verify the correctness of the data-intensive service interaction. Third, the data-related property abstraction is used to refine the DEFSM model through spurious counterexample, partitioning the over-abstracted state into two independent states. Finally, a case study about online ticket sale system is designed to demonstrate the feasibility of our proposed method.


Data-intensive service; Model checking; Spurious counterexample; Abstraction refinement

Citation Format:
Yu-Yu Yin, Hong-Hao Gao, Dong-Jin Yu, "Model-Based Data-Intensive Service Abstraction Refinement," Journal of Internet Technology, vol. 14, no. 5 , pp. 807-816, Sep. 2013.

Full Text:



  • There are currently no refbacks.

Published by Executive Committee, Taiwan Academic Network, Ministry of Education, Taipei, Taiwan, R.O.C
JIT Editorial Office, Office of Library and Information Services, National Dong Hwa University
No. 1, Sec. 2, Da Hsueh Rd., Shoufeng, Hualien 974301, Taiwan, R.O.C.
Tel: +886-3-931-7314  E-mail: