Search

Context: In the past decade, the World Wide Web has been subject to rapid changes. Web sites have evolved from static information pages to dynamic and service-oriented applications that are used for a broad range of activities on a daily basis. For this reason, thorough analysis and verification of Web Applications help assure the deployment of high quality applications. Objectives: In this paper, an approach is presented to the formal verification and validation of existing web applications. The approach consists of using execution traces of a web application to automatically generate a communicating automata model. The obtained model is used to model checking the application against predefined properties, to perform regression testing, and for documentation. Methods: Traces used in the proposed approach are collected by monitoring a web application while it is explored by a user or a program. An automata-based model is derived from the collected traces by mapping the pages of the application under test into states and the links and forms used to browse the application into transitions between the states. Properties, meanwhile, express correctness and quality requirements on web applications and might concern all states of the model; in many cases, these properties concern only a proper subset of the states, in which case the model is refined to designate the subset of the global states of interest. A related problem of property specification in Linear Temporal Logic (LTL) over only a subset of states of a system is solved by means of specialized operators that facilitate specifying properties over propositional scopes in a concise and intuitive way. Each scope constitutes a subset of states that satisfy a propositional logic formula. Results: An implementation of the verification approach that uses the model checker Spin is presented where an integrated toolset is developed and empirical results are shown. Also, Linear Temporal Logic is extended with propositional scopes. Conclusion: a formal approach is developed to build a finite automata model tuned to features of web applications that have to be validated, while delegating the task of property verification to an existing model checker. Also, the problem of property specification in LTL over a subset of the states of a given system is addressed, and a generic and practical solution is proposed which does not require any changes in the system model by defining specialized operators in LTL using scopes.

International audience; Test case prioritisation aims at finding an ordering which enhances a certain property of an ordered test suite. Traditional techniques rely on the availability of code or a specification of the program under test. In this paper, we propose to use string distances on the text of test cases for their comparison and elaborate a prioritisation algorithm. Such a prioritisation does not require code and can be useful for initial testing and in cases when code is difficult to instrument. We also briefly report on preliminary results of an experiment where the proposed prioritisation technique was compared with random permutations and four classical string distance metrics were evaluated.

Test cases are themselves prone to errors, thus techniques and tools to validate tests are needed. In this paper, we suggest a method to check mutual consistency of tests in a test suite.

This chapter addresses the problem of Web application quality assessment from two perspectives. First, it shows the use of model checking of properties formulated in LTL to detect anomalies in Web applications. Anomalies can be derived from standard quality principles or defined for a specific organization or application. The detection is performed on communicating automata models inferred from execution traces. Second, the chapter explains how probabilistic models (Bayesian networks) can be built and used to evaluate quality characteristics. The structure of the networks is defined by refinement of existing models, where the parameters (probabilities and probability tables) are set using expert judgment and fuzzy clustering of empirical data. The two proposed approaches are evaluated and a discussion on how they complement each other is presented.

We consider a formal framework for property verification of web applications using Spin model checker. Some of the web related properties concern all states of the model, while others - only a proper subset of them. To be able to discriminate states of interest in the state space, we solve the problem of property specification in LTL over a subset of states of a system under test while ignoring the valuation of the properties in the rest of them. We introduce specialized operators that facilitate specifying properties over propositional scopes, where each scope constitutes a subset of states that satisfy a propositional logic formula. Using the proposed operators, the user can specify web properties more concisely and intuitively. We illustrate the proposed solution in specifying properties of web applications and discuss other potential applications.

We discuss how specification coverage and fault coverage based test derivation strategies can be combined. In particular, the problem of deriving a test suffix, which raises tester confidence in the configuration of the system, reached after a test derived by a specification coverage criterion, is formalized and solved in the CEFSM setting. The traditional mutant-based test derivation approach is extended with nondeterministic mutants to cover more faults. An experimental tool and case study are reported.