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.