A verification method for web services combination based on abstract and refinement technology

摘要

Model checking has been widely used to verify the compatibility of web services composition model, since it can give counterexample and its high automation. As for the state explosion problem existed in model checking, we introduce the predicate abstraction and refinement technology into the traditional model checking method, and propose a framework for web services composition based on the technology of abstraction and refinement. First, we model each web service with predicate abstraction and composite the models with combination operation. Second, we project the counterexample obtained by model checking over each web service, and confirm the projection counterexample. Third, the web service abstraction model that caused spurious counterexample 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.