Geração de propriedades para o Java pathfinder a partir de objetivos de teste

Resumo

Este projeto BEPE é parte do trabalho de Doutorado financiado pela FAPESP (Processo: 2011/01928-1). O objetivo principal do trabalho de Doutorado é ajudar desenvolvedores de software a aplicar verificação formal na prática. Para isso, propomos uma abordagem que gera o código fonte correspondente às propriedades do sistema que devem ser verificadas para assegurar a qualidade do software. Esta geração de código será guiada pelos objetivos de teste derivados da especificação do sistema.O principal desafio desta pesquisa de Doutorado é sincronizar os propósitos de teste dos níveis de implementação e especificação para automatizar a geração do código das propriedades. Para solucionar este problema, decidimos fazer um trabalho teórico sobre esta sincronização para, então, aplicar os resultados deste trabalho teórico na prática usando o Java PathFinder (JPF), um verificador de modelos que realiza a verificação de programas Java. Neste projeto BEPE, vamos focar na aplicação dos resultados teóricos na prática: nós faremos a implementação de modelos de propriedades genéricas no JPF. Estes modelos serão usados para automatizar a geração de código de propriedades que o sistema precisa satisfazer para garantir sua qualidade. Ademais, o código gerado será registrado no JPF, de modo que ele possa verificar se o sistema satisfaz a propriedade ou não. Para validar a implementação destes modelos de propriedades genéricas no JPF, um conjunto de testes para cada modelo de propriedade será criado e executado. (AU)