Modeling And Verifying Web Applications

Web application is an interactive one with a multi-tier architecture which is complicated, distributed multi-composition and can run at multi-platform and can implemented by multilingual programs. It provides an entirely new way to deploy software applications to end users. Web applications are usually composed of front-end user interfaces in Web browser, back-end servers including web server, application server and database server etc. 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. The analysis and modeling of Web applications are very difficult due to its complexity, dynamicity, heterogeneity and the diversity of its links and compositions. How to ensure the reliability and quality of Web applications introduces new challenges to software engineering community.Testing is a most fundamental approach to improving the reliability and the quality-assurance of software. And model-based testing provides effective ways to implement the testing of Web applications and realizes the automation of test procedure completely. Therefore, it is of the utmost importance to construct appropriate models for model-based Web application testing. This is research emphases in this paper.Modeling of the system lays a foundation and source of the generating test case and testing execution. Whether the models constructed are consistent with users' requirement or not can be verified by model checking. Model checking is an automatic, model-based, property-verification approach and wildly used in automatic verification of finite state systems. 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.This paper focuses on modeling and verifying Web applications available to facilitate to generating test cases. The research work includes: 1. approaches to modeling Web applications by FSM including the Web application portioning and the interactions and compositions of FSM; 2. the formal navigation models of Web applications and the verifications of their consistency and security of navigation; 3. the modeling and verifying Web browser interactions. At last, transforming UML Models to FSM Models has been done. The details are as follows:The most important thing of concerns for model-based testing is to model the Web application. This paper proposes a three-dimensional modeling approach based on FSMs and the concept of Logic Component (LC). We employ a component-interaction automata modeling language (CIAML) to model the interactions between Web pages and back-end servers, software modules and components etc. An approach to modeling the Web page is presented. The model of the whole Web application is modeled by the composition of LCs.From users' view, the navigation behavior in the client-side is a specific feature introduced by Web applications. This paper studies the modeling and verification of Web navigation. Consequently, the key issues lie in formal modeling and properties generation of Web navigation. Kripke structure is one presentation of FSM. An approach to illustrating the navigation using Kripke structure in Web applications is presented, namely, the navigation models are described formally by Kripke structure exploited. The properties to be verified are generated from threefold: design models of Web application, security strategy of Web navigation and users' experience models (UXM). Consistency criterion of Web navigation corresponding to design models and the method to generate verifying properties are laid out. Besides, according to users' experience models, we take Web browser interactions into account and give out verifying properties from UXM. UXM are further used to improve on and modify the design models and navigation models.Web applications can only be accessed through dedicated client systems called Web browsers. The users can press the Back or Forward buttons to negatively influence the behaviors of Web application navigation. Existing navigation models are static ones on the whole. Users' navigation paths are all determined on stage of model design. Web browser interactions that have not been taken into account make them difference from practical navigation in Web applications. Accordingly, special care is taken on Web browser interactions during the user's traversal within hypermedia space in order to specify possible inconsistencies between Web browser interfaces and user cognitions. We give out the concept of Safety Critical Region (SCR) and propose an approach to modeling on-the-fly navigation models.The Kripke structure is employed to describe the on-the-fly navigation models. Coverage criteria of Web browser interactions, such as, node coverage, transition coverage triggered by actions, SCR coverage, are exploited to derive the properties of Web Browser interactions in CTL. Ultimately, we use SMV, the model checking tool, to verify the on-the-fly navigation models.Finally, an approach to transforming UML models to FSM models is proposed. Corresponding transformational rules are presented. We mainly focus on the transformation of UML statecharts to FSM models. First of all, XMI and SCXML are used to describe as texts of UML models and FSM models, respectively. And second, take advantage of the transformation rules, it can automatically implement the transformation between two texts. In this paper we design a model transformer to transform UML models to FSM models.