论文部分内容阅读
Web应用导航行为的建模和验证是可信Web工程研究的重点和难点.在深入分析用户和Web浏览器交互行为的基础上,文中引入On-the-fly策略并基于反例引导的抽象精化验证方法 CEGAR对Web应用的导航行为进行建模和验证.在On-the-fly导航模型展开的过程中,根据检验性质采用增量式状态抽象方法构造Web应用导航抽象模型,通过确认抽象反例来识别伪反例,借助等价类精化方法消除抽象模型上的伪反例.这一方法可有效地缓解Web应用验证过程中出现的状态爆炸问题.
Web application navigation behavior modeling and verification is the key and difficult point of trusted Web engineering research.On the basis of deeply analyzing the interaction between users and Web browser, this paper introduces On-the-fly strategy and abstract refinement guided by counter-examples The verification method CEGAR models and verifies the navigation behavior of Web application.When On-the-fly navigation model is developed, an abstract abstract model of Web application navigation is constructed by using incremental state abstract method according to the nature of inspection, Identify pseudo-counterexamples and eliminate pseudo-counterexamples on abstract models by means of equivalence class refinement.This method can effectively alleviate the state explosion problem in Web application verification process.