Verification And Testing Technology For Web Applications

With prevalence of Internet and rapid development of some technology such as distributed computing, component-based developing and Web services, Web applications have been integrated into many business critical systems and public transaction processing systems. It becomes increasingly important to ensure the quality of Web applications.Two of the most fundamental and important approaches to quality-assurance of software are formal verification and testing. However, a Web application can be considered as a distributed system with multi-tier architecture, it possesses its own unique features such as heterogeneous nature, dynamic behaviors, diversity of connection, changeability in control flow and so on. These features bring new challenges to verification and testing of Web applications. To handle these features, the approaches to verification and testing for traditional applications have to be extended, or some new approaches need to be proposed.Model checking is an automatic, model-based, property-verification approach, and is widely applied to the verification of finite-state system. It analyzes the entire state space of the model in order to determine whether the model violates the properties or not. Model checker produces counterexamples that can be used to diagnose the faults in the system as soon as a violation of the property is detected. Testing is intended to reveal whether or not the expected behavior of a system is consistent with its real behavior. Manual testing is inefficient, error-prone, not documented, not reproducible, and bound to the ingenuity of single engineers. Model checking-based automated testing has got considerable attention in research and industrial communities. To apply model checking to auto-generation of test cases, a key is to construct properties that trap model checker to output counterexamples, and then test cases can be generated from those counterexamples.This paper focuses on model checking-based approaches to formal verification and testing of Web applications by using model checker SMV.The navigation behavior in the client-side is a specific feature introduced by Web applications, so the consistency and safety of navigation are very important quality factors of a Web application. The object relation diagram and the Kripke structure are employed to describe the object structure involved in the navigation of a Web application and the navigation behavior respectively. The relations that are used to both verify and test if the navigation behavior is consistent with the object relation diagram are defined respectively. Both the model checking-based testing approach and verification approach with respect to consistency relations are proposed. An algorithm converting a Kripke structure into SMV program is designed and the prototypes both verifying and testing navigation behaviors are implemented respectively. In addition, the approach to verification according to some common safety policies for navigation is proposed.In server-side, a Web application provides business logic functions and application services by composing components, it is necessary to verify formally the behaviors of component composition in order to assure the quality of a Web application. This paper addresses the state-space explosion problem in the context of verifying component composition. We integrate compositional reasoning into the counterexample guided abstraction refinement (CEGAR) scheme and propose a compositional verification approach such that the verification of component composition is transformed into local abstraction refinement for individual components participating in composition. A theorem about compositional validation is proposed and proved, so validating if a generated counterexample is valid is carried out component-wise by validating the projection of the counterexample on each individual component.One aspect of verification for component composition is checking whether or not the behavior of the composition is safety. This paper proposes a new model, component message automaton, to model interaction behavior of components. Based on controllability from supervisory control theory, the algorithm verifying safety properties of component composition is developed.The objects (Web pages or components) of a Web application is the foundation of navigation and component composition. Based on model checking and data flow testing criteria, this paper proposes an automated approach to test generation for a single object. In case that the source code of an object is unavailable, the dynamic state behavior of the object is modeled by an object state machine, and then the machine is converted into a object flow diagram depicting the control flow and data flow information of the object. We propose an approach to constructing the trap properties according to data flow testing criteria. The testing sequences of an object can be formed by model checking these trap properties against the object flow diagram.Model checking-based testing approaches generate generally a set of counterexamples with much redundancy. An on-the-fly approach to test generation and optimization is proposed. When a new counterexample is generated along with model checking for a property, the counterexample is used to detect redundant properties, and is also winnowed by the set of test generated before.