doi: 10.4304/jsw.9.4.793-799
Web Service Composition Verification of Safety Properties Based on Predicate Abstraction
- 1 Science School, Xi’an University of Architecture and Technology, Xi’an 710055, China
- 2 The School of Automation, Northwestern Polytechnical University, Xi'an, Shaanxi, China
Abstract
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.
Keywords
- model checking
- web service composition
How to Cite
Yuying Wang and Ning Yang, "Web Service Composition Verification of Safety Properties Based on Predicate Abstraction," Journal of Software, vol. 9, no. 4, pp. 793-799, 2014. https://doi.org/ 10.4304/jsw.9.4.793-799
Copyright & License
Copyright © 2014 by the authors. This is an open access article distributed under the Creative Commons Attribution License which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited (CC BY 4.0).