• JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
 
  Bookmark and Share
 
 
Dissertação de Mestrado
DOI
https://doi.org/10.11606/D.45.2004.tde-20220712-121325
Documento
Autor
Nome completo
Leandro César Prudente
E-mail
Unidade da USP
Área do Conhecimento
Data de Defesa
Imprenta
São Paulo, 2004
Orientador
 
Título em português
Um estudo sobre teste versus verificação formal de programas Java
Palavras-chave em português
Engenharia De Software
Resumo em português
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.
 
Título em inglês
not available
Resumo em inglês
not available
 
AVISO - A consulta a este documento fica condicionada na aceitação das seguintes condições de uso:
Este trabalho é somente para uso privado de atividades de pesquisa e ensino. Não é autorizada sua reprodução para quaisquer fins lucrativos. Esta reserva de direitos abrange a todos os dados do documento bem como seu conteúdo. Na utilização ou citação de partes do documento é obrigatório mencionar nome da pessoa autora do trabalho.
Data de Publicação
2022-07-13
 
AVISO: Saiba o que são os trabalhos decorrentes clicando aqui.
Todos os direitos da tese/dissertação são de seus autores.
CeTI-SC/STI
© 2001-2024. Biblioteca Digital de Teses e Dissertações da USP.