基于CEGAR的Web应用验证  

Verification of Web Application Based on CEGAR Approach

作　　者：高洪皓[1,2,3] 缪淮扣[1,3] 曾红卫[1] 

机构地区：[1]上海大学计算机工程与科学学院,上海 200444 [2]上海大学计算中心,上海 200444 [3]上海市计算机软件评测重点实验室,上海 201114

出　　处：《计算机学报》2014年第4期976-992,共17页Chinese Journal of Computers

基　　金：国家自然科学基金(61170044,61073050,61262010)资助~~

摘　　要：Web应用导航行为的建模和验证是可信Web工程研究的重点和难点.在深入分析用户和Web浏览器交互行为的基础上,文中引入On-the-fly策略并基于反例引导的抽象精化验证方法 CEGAR对Web应用的导航行为进行建模和验证.在On-the-fly导航模型展开的过程中,根据检验性质采用增量式状态抽象方法构造Web应用导航抽象模型,通过确认抽象反例来识别伪反例,借助等价类精化方法消除抽象模型上的伪反例.这一方法可有效地缓解Web应用验证过程中出现的状态爆炸问题.How to model and verify navigational behaviors of Web application is the key issue toensure the reliability of Web engineering.After analyzing the interactive behaviors between theuser and Web browser,this paper applies On-the-fly strategy and Counterexample-GuidedAbstraction Refinement （CEGAR）method to Web application modeling,abstraction refinement andverification.When the navigation model is constructed on the fly,a verification property basedincremental state abstraction approach is proposed to generate the corresponding abstract naviga-tion model.Then,an equivalence classes-based abstraction refinement is introduced to eliminatethe 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.

关 键 词：WEB应用 导航模型 抽象精化 模型检验 伪反例 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]