Integração entre verificação de modelos e teste de software para melhoria da detecção de erros em sistemas computacionais

Abstract

Os sistemas de computação estão presentes em diversas atividades de vital importância atualmente. Por este fato, a verificação do comportamento de aplicações é uma tarefa fundamental para se garantir a conformidade da execução das aplicações com seu comportamento esperado. Mesmo com técnicas formais, não é possível garantir completamente o comportamento correto de uma aplicação, mas consegue-se aumentar a confiança sobre a sua correta execução. Este trabalho busca estabelecer um algoritmo que integre as técnicas de verificação de modelos e teste de software. Este algoritmo deve aumentar a cobertura dos testes e, ao mesmo tempo, melhorar a completude de um modelo abstrato do comportamento da aplicação. Desta forma, é possível encontrarem-se eventuais problemas com o código da aplicação através de um procedimento automático e que possa ser repetido onde, gradualmente, se melhora a cobertura oferecida pelas duas técnicas utilizadas. Esta integração é feita através do uso de modelos de comportamento gerados partindo-se de um conjunto inicial de testes, através de uma técnica de extração de modelos. Após a geração de um modelo inicial, o modelo é verificado contra um conjunto de propriedades. Em caso de violações, novos casos de testes são gerados para garantir que os problemas encontrados são erros reais. Em caso de erros espúrios, o modelo é refinado para eliminar o comportamento inválido. Quando o modelo está correto, começa-se a gerar novos testes, baseados no modelo, para aumentar a cobertura de testes sobre a aplicação. Espera-se que durante este processo se identifiquem novos possíveis problemas na aplicação para que se possa corrigi-los. Validou-se o algoritmo em estudos de caso, conseguindo-se executá-lo de forma parcialmente automática. Alguns problemas reais foram identificados e corrigidos. Adicionalmente, um conjunto de novos testes foi gerado e a completude do modelo foi aumentada, assim atingindo o objetivo do algoritmo.

Software systems are present in almost every crucial daily activity nowadays. For this reason verifying the behavior of a given software system is fundamental to guarantee the conformance between the intended behavior and the actual execution of the given application. Even when formal methods are used, it is not possible to completely ensure the correct behavior of an application, however it is possible to increase the confidence on the correct behavior of that given application. This work tries to establish an algorithm that integrates Model Checking and Software testing. This algorithm should increase the testing coverage and, at the same time, be able to increase the completeness of a given abstract behavior model of the application. This way, one can discover errors in the application through an automatic and reproducible method that can gradually increase the coverage provided by the applied techniques. This integration is performed through behavior models generated using a model extraction approach base on a set of test cases. After generating the initial model, this model is checked against a set of properties of interest to ensure its correctness. When a violation occurs, a set of test cases is generated to check whether it is a real violation. If a spurious violation is detected, the model is refined to eliminate the invalid behavior. When the model is considered correct, new test cases are created based on that model in order to increase the testing coverage of the application. It is expected that during that process new errors are identified so that one can fix them. The algorithm was validated through case studies and was executed in a semi-automatic way. A given set of real application errors was identified and fixed. In addition to that, a set of new test cases was produced increasing the testing coverage of the application, thus reaching the expected result for the algorithm.