Localização de falhas em programas concorrentes em C
Este trabalho descreve uma nova abordagem para localizar falhas em programas concorrentes, a qual é baseada em técnicas de verificação de modelos limitada e sequencialização. A principal novidade dessa abordagem é a ideia de reproduzir um comportamento defeituoso em uma versão sequencial do programa...
| Autor principal: | Alves, Erickson Higor da Silva |
|---|---|
| Outros Autores: | http://lattes.cnpq.br/6589284404023306 |
| Grau: | Dissertação |
| Idioma: | por |
| Publicado em: |
Universidade Federal do Amazonas
2018
|
| Assuntos: | |
| Acesso em linha: |
https://tede.ufam.edu.br/handle/tede/6788 |
| Resumo: |
|---|
|
Este trabalho descreve uma nova abordagem para localizar falhas em programas concorrentes, a qual é baseada em técnicas de verificação de modelos limitada e sequencialização. A principal novidade dessa abordagem é a ideia de reproduzir um comportamento defeituoso em uma versão sequencial do programa concorrente. De forma a apontar linhas defeituosas, analizam-se os contraexemplos gerados por um verificador de modelos para o programa sequencial instrumentado e procura-se um valor para uma variável de diagnóstico, o qual corresponde a linhas reais no programa original. Essa abordagem é útil para aperfeiçoar o processo de depuração para programas concorrentes, já que ela diz qual linha deve ser corrigida e quais valores levam a uma execução bem-sucedida. Essa abordagem foi implementada como uma transformação código-a-código de um programa concorrente para um não-determinístico sequencial, o qual é então usado como entrada para ferramentas de verificação existentes. Resultados experimentais mostram que a abordagem descrita é eficaz e é capaz de localizar falhas na maioria dos casos de teste utilizados, extraídos da suíte da International Competition on Software Verification 2015. |