Model-Based Verification and Testing of Web Services: Functionality, Robustness and Vulnerability Analysis

Faezeh Siavashi

    Forskningsoutput: Typer av avhandlingarDoktorsavhandlingSamling av artiklar


    Web services are software systems that are designed to support machine-to-machine interactions over a network. These services enable people to access a wide variety of resources through their personal computers or mobile devices. Nowadays, most of the traditional business activities and manual services are being enhanced by web services.

    When using web services, users expect that not only they are continually available, but also they work correctly and provide secure access to data. However, ensuring the quality of web service implementations is not simple for several reasons. First, they are accessible using public communication protocols from anywhere in the world by a large number of users. Therefore, web services should be robust enough to be able to accept correct input and reject incorrect and malicious ones. Secondly, the reputation of web services greatly depends on how they perform as expected while securing users' data. Finally, the implementation of web services should be developed in such a way that it can ensure access control of users. Implementing new features or modifying a developed feature requires additional attention to ensure that access control is not altered.

    Software testing is one of the techniques used for quality assurance of software systems. In software testing in which a set of inputs is provided to the system under test and the outputs produced are compared against the expected outputs. Testing is typically a largely informal process, which in many cases is left at the end of the software development process and reduced to fit the project deadlines. Thus, there is a need to deploy novel testing methods that will make testing of web services both efficient and effective.

    In this thesis, we define a model-based testing approach to evaluate the behavior of web services and their compositions. The goal of using models is to introduce a verifiable specification of the web service that is used later on to generate tests that are executed against the implementation of the web service. In our approach, we use model checking to make sure that the requirements of the web service are satisfied by the model-based specification. Then, we use model-based testing to check that the implementation of the web service corresponds to verified specifications, and consequently to its requirements.

    As a first step, we study how the interaction of the web service with their environment can be modeled and used for test generation. To this extent, we conduct a systematic literature review on the use of environment models in model-based testing. Then, we provide a first approach in which the interactions of web services with their environment are modeled with UML sequence diagrams, while the behavior of the web services is specified with UML state machines. Both models are transformed into UPPAAL Timed Automata, to verify that the behavior of the services allows the specified interactions. Besides, we verify that different requirements of the web service are satisfied. The resulting verified model is used for online test generation against the implementation of the web service.

    As another contribution of this thesis, we define an approach to assess the robustness and security vulnerabilities of web services in the presence of unexpected or invalid conditions and inputs. To that extent, we extend our previous MBT approach in the context of mutation testing. In model-based mutation testing, the original test model is altered via mutation operators to provide slightly incorrect behavior. The mutant models are used to generate tests that will provide invalid test inputs to evaluate how robust the service implementation is to such inputs and if any security vulnerabilities are exposed.

    Furthermore, we extend the above approach with two contributions. We first define a set of mutation operators for UPPAAL timed automata and we evaluate them empirically in the context of web services. Then, we propose a novel mutation-selection technique that eliminates the mutant models that are not useful for testing and we, consequently, reduce the test execution time. The results show that these techniques increase the efficiency and effectiveness of our approach.

    In this thesis, several tools that facilitate testing activities support the testing approach. In some cases, we used existing tools like the UPPAAL model checker and the UPPAAL TRON test generator. In other cases, we have complemented the existing toolset with new tools. Notably, for the mutation testing approach, we implemented a tool called μUTA, which automates the mutant generation, mutant-selection, and mutant execution processes.

    The approaches defined in this thesis have been applied in two case studies. The results show that our testing methodology can create test cases that explore the behavior of the systems extensively and reveal new faults that remain undetected by traditional model-based testing methods.

    • Truscan, Dragos, Handledare
    Tryckta ISBN978-952-12-3935-9
    Elektroniska ISBN978-952-12-3936-6
    StatusPublicerad - 2020
    MoE-publikationstypG5 Doktorsavhandling (artikel)


    • model-based mutation testing
    • Model-based Testing
    • UPPAAL
    • UML
    • UPPAAL Timed Automata
    • Web services
    • Software Testing

    Citera det här