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