Verification of Web Application Based on CEGAR Approach
Gao Hong · Chinese Journal of Computers · 2014
How to model and verify navigational behaviors of Web application is the key issue to ensure the reliability of Web engineering.After analyzing the interactive behaviors between the user and Web browser,this paper applies On-the-fly strategy and Counterexample-Guided Abstraction Refinement(CEGAR)method to Web application modeling,abstraction refinement and verification.When the navigation model is constructed on the fly,a verification property based incremental state abstraction approach is proposed to generate the corresponding abstract navigation model.Then,an equivalence classes-based abstraction refinement is introduced to eliminate the spurious counterexample if the abstract counterexample is proven to be false.In conclusion, our approach can effectively alleviate the state explosion problem of Web application verification.