Thesis detail

Authors: Cristiá, Maximiliano.

Summary: The most resource-consuming phase of software production is the verification of its qualities, including functional correctness. However, due to its costs, the software industry seldom performs a thorough verification of its products. One of the most promising strategies to reduce the costs of software verification is making it as automatic as possible. Currently, this industry relies basically only on testing to verify functional correctness. Therefore, we sought to automate functional testing of software systems by providing tool support for the test case generation step. Model-based testing (MBT) is a testing theory that has achieved impressive successes in automating the testing process. Any MBT method analyses a formal model or specification of the system under test to generate test cases that later are executed on the system. Almost all methods work with some form of finite state machines (FSM) which limits their application since FSM´s cannot describe general systems. However, a great advantage of these methods is that they reach a high degree of automation. In this thesis we show, on the contrary, the degree of automation we have achieved by applying a MBT method, known as Test Template Framework (TTF), to Z specifications. Since Z is based on first-order logic and set theory it is far more expressive than FSM´s, thus making our results applicable to a wider range of programs. During this thesis we have improved the TTF and developed a tool, called Fastest, that implements all of our ideas. Fastest provides tool support for the following activities: -Partitioning of the input space of Z operations.-Building testing trees.-Elimination of inconsistent test specifications.-Generation of abstract test cases.

Academic degree: Universitario de posgrado/doctorado.

Obtained title: Doctor en informática.

Language: Inglés.

Knowledge area: Ciencias de la Computación.

Year: 2012