Geração de Propriedades sobre Programas Java a partir de Objetivos de Teste

• Processo: 11/01928-1
• Modalidade de apoio: Bolsas no Brasil - Doutorado
• Data de Início da vigência: 01 de julho de 2011
• Data de Término da vigência: 17 de julho de 2015
• Área de conhecimento: Ciências Exatas e da Terra - Ciência da Computação - Metodologia e Técnicas da Computação
• Pesquisador responsável: Ana Cristina Vieira de Melo
• Beneficiário: Simone Hanazumi
• Instituição Sede: Instituto de Matemática e Estatística (IME). Universidade de São Paulo (USP). São Paulo , SP, Brasil
• Bolsa(s) vinculada(s): 13/22317-6 - Geração de propriedades para o Java pathfinder a partir de objetivos de teste, BE.EP.DR
• Assunto(s): Engenharia de software Java
• Palavra(s)-Chave do Pesquisador: Especificação de Programas | java | Objetivos de Teste | Verificação Formal | Engenharia de Software

Resumo

Com a presença cada vez maior de sistemas computacionais e novas tecnologias no cotidiano das pessoas, garantir que eles não falhem e funcionem corretamente tornou-se algo de extrema importância. Além de indicar a qualidade do sistema, assegurar seu bom funcionamento é essencial para se evitar perdas, desde financeiras até de vidas.Uma das técnicas utilizadas para esta finalidade é a chamada verificação formal de programas. A partir da especificação do sistema, descrita numa linguagem formal, são definidas propriedades a serem satisfeitas e que certificariam a qualidade do software. Estas propriedades devem então ser implementadas para uso num verificador, que é a ferramenta responsável por executar a verificação e informar quais propriedades foram satisfeitas e quais não foram, indicando aos desenvolvedores os possíveis locais com código incorreto no sistema.A desvantagem do uso da verificação formal é, além do seu alto custo, a necessidade de haver pessoas com treinamento em linguagens e métodos formais. Ademais, a implementação de propriedades relativas a um sistema em particular para uso num verificador é uma tarefa complexa e custosa.Para auxiliar os desenvolvedores na utilização da verificação formal em programas escritos em Java, este trabalho propõe a geração de código de propriedades para uso direto no verificador, a partir de objetivos de testes derivados dos requisitos formais de sistemas.

Publicações científicas

(Referências obtidas automaticamente do Web of Science e do SciELO, por meio da informação sobre o financiamento pela FAPESP e o número do processo correspondente, incluída na publicação pelos autores)

HANAZUMI, SIMONE; DE MELO, ANA C. V.. A Formal Approach to implement java exceptions in cooperative systems. JOURNAL OF SYSTEMS AND SOFTWARE, v. 131, p. 475-490, SEP 2017. (13/22317-6, 12/23767-2, 11/01928-1)

Publicações acadêmicas

(Referências obtidas automaticamente das Instituições de Ensino e Pesquisa do Estado de São Paulo)

HANAZUMI, Simone. Geração de propriedades sobre programas Java a partir de objetivos de teste. 2015. Tese de Doutorado - Universidade de São Paulo (USP). Instituto de Matemática e Estatística (IME/SBI) São Paulo.