| Name: | Description: | Size: | Format: | |
|---|---|---|---|---|
| 938.25 KB | Adobe PDF |
Authors
Advisor(s)
Abstract(s)
O teste de software é o principal modo de veri car a correção deste. Normalmente constitui
50% do seu custo de desenvolvimento. Existem diversas estratégias de teste de software mas,
nesta dissertação, é essencialmente abordado o teste unitário, uma forma de teste que permite
a análise de pequenos componentes individuais do sistema (funções, classes ou módulos).
O seu principal objetivo é detetar erros lógicos nos componentes, veri car corner cases e tentar
obter a maior cobertura de código testado possível. O grande problema desta abordagem é ser,
normalmente, um processo manual, o que por sua vez o torna dispendioso, propício a erros e
bastante demorado. Portanto seria uma mais valia conseguir automatizar o processo de geração
e execução do teste unitário com uma elevada cobertura de código.
Nesta dissertação é apresentado e explorado o conceito de testes Concolic com o intuito de
permitir ultrapassar algumas das limitações anteriormente mencionadas. O teste Concolic junta
duas técnicas de teste de software: teste com valores concretos e simbólicos simultaneamente.
Atualmente existem várias ferramentas que permitem realizar este tipo de teste de software e
esta dissertação inspira-se sobre uma delas.
O principal foco desta dissertação foi a exploração e possível integração de uma ferramenta
de teste Concolic no Frama-C. O Frama-C, implementado em Objective Caml (Ocaml), disponibiliza
um conjunto de ferramentas dedicadas a análise de código C. Fornece várias técnicas
de análise estática numa única framework e é usado atualmente por empresas como Airbus e
Dassault Aviation.
Deste modo foram analisadas e estudadas um conjunto de ferramentas que permitissem realizar
teste Concolic. Posteriormente foi escolhida uma ferramenta (Crest) com o intuito adaptar os
seus processo à plataforma Frama-C e à respetiva implementação em Ocaml. Esta ferramenta
permite a execução de testes Concolic de programas desenvolvidos na Linguagem C e contempla
várias etapas:
1. Inicialmente é feita automaticamente a instrumentação do código, isto é, altera-se o
código original para um código que realize chamadas a funções que permitam a sua execu
ção simbólica. Se o programa for fornecido com valores concretos, este produz o mesmo
output que o original. Esta etapa é feita através do Common Intermediate Language (CIL).
2. Finda a instrumentação é feito um ciclo de execução em que são armazenadas um conjunto
de restrições das várias condições encontradas. Estas condições são armazenadas
e posteriormente resolvidas, fazendo uso do Yices, e assim gerar novos valores para, na
próxima execução, percorrer diferentes caminhos.
O resultado nal desta dissertação contempla a adaptação dos principais funamentos do Crest
a uma implementação OCaml e respetiva integração em Frama-C. Todas as etapas foram implementadas
desde as várias etapas da instrumentação à execução dos testes, geração automática
de inputs e integração no Frama-C.
Software testing is the main mechanism for verifying the soundness of any software. There are several strategies for doing it. This thesis focuses, primarily, on unit testing, which allows the veri cation of the smallest components of the system (functions, classes or modules). The main objective of this type of test is to detect logical errors in those components, to verify corner cases and to try to obtain the largest coverage of tested code as possible. However, there are problems associated. Usually, the biggest issue involved is that this type of testing has to be done manually, which makes the process expensive, error prone and time consuming. Therefore, it would be extremely useful to automatize the generation and execution process of unit testing. This thesis will present and explore the concept of unit testing with the purpose of allowing to overcome some of the above mentioned limitations of this activity. Concolic testing establishes a connection between two software testing techniques: the testing with concrete and symbolic values, simultaneously. Currently, there are several tools available which allow this type of testing and this thesis is inspired in one of these tools. The main focus of this thesis was the exploration and possible integration of a Concolic testing tool in Frama-C. The Frama-C, implemented in OCaml, offers a range of tools dedicated to the analyse of C code. It provides several analysis techniques in one framework and it’s used nowadays by companies such as Airbus and Dassault Aviation. Thus, a set of tools that make it possible the execution of Concolic tests was studied and analysed. Later, Crest was chosen as a reference implementation of a Concolic test tool with the purpose of implementing it in OCaml and to integrate in Frama-C. The latter makes it possible the execution of Concolic tests of programs developed in C language and contemplates several stages: 1. Initially, we proceed to the code instrumentation, which means that the original code is changed for another one that performs calls to functions that allow the symbolic execution. If the program is furnished with concrete values, this produces the same output as the original does. This step is done using Common Intermediate Language (CIL). 2. When the instrumentation process ends, a new cycle of execution is done, where a whole set of constraints of the conditions that the code may contain are stored and solved, through Yices, to make it possible the generation of new values and go through different paths in the next execution. The nal result of this thesis contemplates the adaptation of the main fundamentals of Crest to an OCaml implementation and its respective integration in Frama-C. All the stages were implemented from the various instrumentation steps until tests execution, automatic generation of inputs and integration in Frama-C.
Software testing is the main mechanism for verifying the soundness of any software. There are several strategies for doing it. This thesis focuses, primarily, on unit testing, which allows the veri cation of the smallest components of the system (functions, classes or modules). The main objective of this type of test is to detect logical errors in those components, to verify corner cases and to try to obtain the largest coverage of tested code as possible. However, there are problems associated. Usually, the biggest issue involved is that this type of testing has to be done manually, which makes the process expensive, error prone and time consuming. Therefore, it would be extremely useful to automatize the generation and execution process of unit testing. This thesis will present and explore the concept of unit testing with the purpose of allowing to overcome some of the above mentioned limitations of this activity. Concolic testing establishes a connection between two software testing techniques: the testing with concrete and symbolic values, simultaneously. Currently, there are several tools available which allow this type of testing and this thesis is inspired in one of these tools. The main focus of this thesis was the exploration and possible integration of a Concolic testing tool in Frama-C. The Frama-C, implemented in OCaml, offers a range of tools dedicated to the analyse of C code. It provides several analysis techniques in one framework and it’s used nowadays by companies such as Airbus and Dassault Aviation. Thus, a set of tools that make it possible the execution of Concolic tests was studied and analysed. Later, Crest was chosen as a reference implementation of a Concolic test tool with the purpose of implementing it in OCaml and to integrate in Frama-C. The latter makes it possible the execution of Concolic tests of programs developed in C language and contemplates several stages: 1. Initially, we proceed to the code instrumentation, which means that the original code is changed for another one that performs calls to functions that allow the symbolic execution. If the program is furnished with concrete values, this produces the same output as the original does. This step is done using Common Intermediate Language (CIL). 2. When the instrumentation process ends, a new cycle of execution is done, where a whole set of constraints of the conditions that the code may contain are stored and solved, through Yices, to make it possible the generation of new values and go through different paths in the next execution. The nal result of this thesis contemplates the adaptation of the main fundamentals of Crest to an OCaml implementation and its respective integration in Frama-C. All the stages were implemented from the various instrumentation steps until tests execution, automatic generation of inputs and integration in Frama-C.
Description
Keywords
Teste Concolic Teste Software Frama-C Execução Simbólica Execução Concreta Pesquisa de Bugs Teste Unitário