Detalhes bibliográficos
| Ano de defesa: |
2004 |
| Autor(a) principal: |
Prudente, Leandro César |
| Orientador(a): |
Não Informado pela instituição |
| Banca de defesa: |
Não Informado pela instituição |
| Tipo de documento: |
Dissertação
|
| Tipo de acesso: |
Acesso aberto |
| Idioma: |
por |
| Instituição de defesa: |
Biblioteca Digitais de Teses e Dissertações da USP
|
| Programa de Pós-Graduação: |
Não Informado pela instituição
|
| Departamento: |
Não Informado pela instituição
|
| País: |
Não Informado pela instituição
|
| Palavras-chave em Português: |
|
| Link de acesso: |
https://teses.usp.br/teses/disponiveis/45/45134/tde-20220712-121325/
|
Resumo: |
Neste trabalho, estabelecemos uma correspondência entre a atividade de teste e a verificação formal de propriedades para programas concorrentes Java. Para tanto, aplicamos um dos critérios baseados no fluxo de objetos (critério de todos os pares definição-uso de objetos) e a ferramenta de verificação Bandera. A prioridade verificada é a ausência de deadlock. O estudo foi feito para analisar a cobertura dos requisitos identificados de cada programa, segundo o critério de teste adotado. Esta análise foi feita sobre 10 programas que apresentam o deadlock e logo em seguida sobre estes mesmos programas com a retirada do deadlock. Quando a propriedade é violada, a análise é realizada sobre os contra-exemplos gerados pela Bandera. Por outro lado, quando a propriedade não é violada, a análise é feita sobre os estados exercitados. Através deste estudo, percebemos que o uso de uma ferramenta de verificação formal é útil para auxiliar a cobertura do critério definido. Além disso, também mostramos que a análise de programas com e sem deadlock são complementares, ou seja, requisitos que não foram exercitados com a violação da propriedade foram exercitados quando esta não foi violada e vice-versa. |
