Abstract:

Model checking has been widely used to verify the compatibility of Web services composition models, since it can give counterexamples and high automation. As for the state explosion problem existing in model checking, we introduce the predicate abstraction and refinement techniques into the traditional model checking method, and propose a framework for Web services composition based on the such techniques. First, we model each Web service based on the predicate abstraction and composite the models with combination operations. Second, we project the counterexamples obtained by model checking over each Web service, and confirm the projection counterexamples. Third, the Web service abstraction model that causes spurious counterexamples is refined, and a new composition abstract model, whose properties also should be verified, is generated. Finally, we show the correctness of our proposal to relieve state explosion.

Key words: Web services combination;model checking;predicate abstraction;refinement technique