基于犆犈犌犃犚的犠犲犫应用验证

• 作者: 曾红卫 缪淮扣 高洪皓
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: Web应用 导航模型 抽象精化 模型检验 伪反例
• 年，卷（期）: 2014,（4）
• 所属期刊栏目: 互联网技术
• 页码范围: 976-992
• 页数: 17页
• 分类号: TP311
• 字数: 16371字
• 语种: 中文
• DOI: 10.3724/SP.J.1016.2014.00976

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	缪淮扣	上海大学计算机工程与科学学院	100	1030	16.0	26.0
3	曾红卫	上海大学计算机工程与科学学院	31	341	11.0	17.0
6	高洪皓	上海大学计算机工程与科学学院	35	118	6.0	8.0