|
|||||
|
|
| 基于CEGAR的Web应用验证 | |
| 引用本文： | 高洪皓,缪淮扣,曾红卫.基于CEGAR的Web应用验证[J].计算机学报,2014(4):976-992. |
| 作者姓名： | 高洪皓 缪淮扣 曾红卫 |
| 作者单位： | 上海大学计算机工程与科学学院;上海大学计算中心;上海市计算机软件评测重点实验室 |
| 基金项目： | 国家自然科学基金(61170044,61073050,61262010)资助~~ |
| 摘 要： | Web应用导航行为的建模和验证是可信Web工程研究的重点和难点.在深入分析用户和Web浏览器交互行为的基础上,文中引入On-the-fly策略并基于反例引导的抽象精化验证方法 CEGAR对Web应用的导航行为进行建模和验证.在On-the-fly导航模型展开的过程中,根据检验性质采用增量式状态抽象方法构造Web应用导航抽象模型,通过确认抽象反例来识别伪反例,借助等价类精化方法消除抽象模型上的伪反例.这一方法可有效地缓解Web应用验证过程中出现的状态爆炸问题. |
| 关 键 词： | Web应用 导航模型 抽象精化 模型检验 伪反例 |
| 本文献已被 CNKI 等数据库收录！ | |