基于CEGAR的Web应用验证

作     者：高洪皓 缪淮扣 曾红卫 GAO Hong-Hao;MIAO Huai-Kou;ZENG Hong-Wei

作者机构：上海大学计算机工程与科学学院上海 200444 上海大学计算中心上海 200444 上海市计算机软件评测重点实验室上海 201114 

出 版 物：《计算机学报》 (Chinese Journal of Computers)

年 卷 期：2014年第37卷第4期

页      面：976-992页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

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

主　　题：Web应用 导航模型 抽象精化 模型检验 伪反例 

摘      要：Web应用导航行为的建模和验证是可信Web工程研究的重点和难点.在深入分析用户和Web浏览器交互行为的基础上,文中引入On-the-fly策略并基于反例引导的抽象精化验证方法 CEGAR对Web应用的导航行为进行建模和验证.在On-the-fly导航模型展开的过程中,根据检验性质采用增量式状态抽象方法构造Web应用导航抽象模型,通过确认抽象反例来识别伪反例,借助等价类精化方法消除抽象模型上的伪反例.这一方法可有效地缓解Web应用验证过程中出现的状态爆炸问题.