Model Checking-Based Testing of Web Applications

摘要

A formal model representing the navigation behaviorof a Web application as the Kripke structure is proposed and anapproach that applies model checking to test case generation ispresented. The Object Relation Diagram as the object model isemployed to describe the object structure of a Web applicationdesign and can be translated into the behavior model. A key problem of model checking-based test generation for a Web application is how to construct a set of trap properties that intend to causethe violations of model checking against the behavior model andoutput of counterexamples used to construct the test sequences.We give an algorithm that derives trap properties from the objectmodel with respect to node and edge coverage criteria.