Busca avançada
Ano de início
Entree

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

Processo: 13/22317-6
Linha de fomento:Bolsas no Exterior - Estágio de Pesquisa - Doutorado
Vigência (Início): 17 de março de 2014
Vigência (Término): 17 de janeiro de 2015
Área do 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
Supervisor no Exterior: Corina Pasareanu
Instituição-sede: Instituto de Matemática e Estatística (IME). Universidade de São Paulo (USP). São Paulo , SP, Brasil
Local de pesquisa : Carnegie Mellon University (CMU), Estados Unidos  
Vinculado à bolsa:11/01928-1 - Geração de propriedades sobre programas Java a partir de objetivos de teste, BP.DR
Assunto(s):Java   Engenharia de software

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)

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. Citações Web of Science: 0.

Por favor, reporte erros na lista de publicações científicas escrevendo para: cdi@fapesp.br.