Model-Based Data-Intensive Service Abstraction Refinement

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

國際替代計量

全文下載

主題瀏覽