On-the-fly策略下的Web应用导航行为验证与抽象精化

"基于CEGAR的Web应用验证" 这篇论文关注的是Web应用验证的问题，特别是在Web应用导航行为的建模和验证方面。Web应用的复杂性和安全性需求使得这一领域成为可信Web工程的重要研究点。文章的核心是采用了反例引导的抽象精化验证方法（CEGAR），即Counterexample-Guided Abstraction Refinement，这是一种用于解决模型检查问题的有效策略。 CEGAR方法在Web应用的上下文中结合了On-the-fly策略。On-the-fly策略允许在模型展开的过程中动态地处理和优化模型，减少了不必要的计算和存储开销。在Web应用导航模型的构建过程中，此策略能够根据需要逐步增加细节，以实现更精确的模型。 文章中提到，作者们基于检验性质采用增量式状态抽象方法来构建Web应用的导航抽象模型。这种抽象方法有助于简化模型，降低状态空间的复杂性。然而，抽象过程中可能会产生“伪反例”，即看似违反性质但实际上并不违反的示例。为了解决这个问题，他们利用等价类精化技术来识别和消除这些伪反例，确保验证的准确性。 通过这种方法，状态爆炸问题得到有效缓解，这是在模型检查中常见的挑战，尤其是在处理大型或复杂系统时。状态爆炸是指随着系统状态数量的指数增长，验证的难度和资源需求急剧上升。CEGAR通过迭代的抽象和细化过程，只考虑必要的状态，从而避免了状态空间的无谓膨胀。 该研究工作得到了国家自然科学基金的支持，由高洪皓、缪淮扣和曾红卫三位研究人员共同完成。他们的研究背景涵盖了模型检验、Web应用和服务计算，以及软件工程和形式化方法等领域。 关键词包括Web应用、导航模型、抽象精化、模型检验和伪反例，这些都直接关联到论文的主要内容和技术手段。这篇论文提出了一种利用CEGAR和On-the-fly策略来有效验证Web应用导航行为的方法，旨在提高Web应用的安全性和可靠性，同时降低验证的复杂度。