CAJ | 학술논문

Web应用导航行为的建模和验证是可信Web工程研究的重点和难点。在深入分析用户和Web浏览器交互行为的基础上，文中引入On-the-fly策略并基于反例引导的抽象精化验证方法CEGAR对Web应用的导航行为进行建模和验证。在On-the-fly导航模型展开的过程中，根据检验性质采用增量式状态抽象方法构造Web应用导航抽象模型，通过确认抽象反例来识别伪反例，借助等价类精化方法消除抽象模型上的伪反例。这一方法可有效地缓解Web应用验证过程中出现的状态爆炸问题。
Web응용도항행위적건모화험증시가신Web공정연구적중점화난점。재심입분석용호화Web류람기교호행위적기출상，문중인입On-the-fly책략병기우반례인도적추상정화험증방법CEGAR대Web응용적도항행위진행건모화험증。재On-the-fly도항모형전개적과정중，근거검험성질채용증량식상태추상방법구조Web응용도항추상모형，통과학인추상반례래식별위반례，차조등개류정화방법소제추상모형상적위반례。저일방법가유효지완해Web응용험증과정중출현적상태폭작문제。
How to model and verify navigational behaviors of Web application is the key issue toensure the reliability of Web engineering.After analyzing the interactive behaviors between theuser and Web browser,this paper applies On-the-fly strategy and Counterexample-GuidedAbstraction Refinement (CEGAR)method to Web application modeling,abstraction refinement andverification.When the navigation model is constructed on the fly,a verification property basedincremental state abstraction approach is proposed to generate the corresponding abstract naviga-tion model.Then,an equivalence classes-based abstraction refinement is introduced to eliminatethe spurious counterexample if the abstract counterexample is proven to be false.In conclusion,our approach can effectively alleviate the state explosion problem of Web application verification.