Web Service Composition Verification of Safety Properties Based on Predicate Abstraction

摘要

State space explosion is one of the biggest problemin model checking. Predicate abstraction technique is used toreduce the size of state space of colored Petri net models, andan algorithm was proposed to obtain the abstracted statespace of a colored Petri net model without its original statespace generated. A method to verify safety properties of Webservice composition by abstracted state space and theCounterexample-Guided Abstraction Refinement wasproposed. The problem of state space explosion is solved tosome extend by this way. Finally, with an example, anapplication of this method is illustrated, which its efficiencyshown.