VVTransv: um método para teste e verificação formal transversal ao desenvolvimento de sistemas críticos

• Processo: 12/23767-2
• Modalidade de apoio: Auxílio à Pesquisa - Regular
• Data de Início da vigência: 01 de agosto de 2013
• Data de Término da vigência: 31 de julho de 2016
• Á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: Ana Cristina Vieira de Melo
• Instituição Sede: Instituto de Matemática e Estatística (IME). Universidade de São Paulo (USP). São Paulo , SP, Brasil
• Pesquisadores associados: Nandamudi Lankalapalli Vijaykumar ; Valdivino Alexandre de Santiago Júnior
• Bolsa(s) vinculada(s): 13/27112-3 - Definição de novas abordagens de análise de eficiência de suites de teste, BP.TT; 13/25309-4 - Geração de requisitos de teste para sistemas espaciais, BP.TT; 13/19814-8 - Estudo comparativo entre modelos de teste e verificação, BP.TT
• Assunto(s): Desenvolvimento de software Teste e avaliação de software Validação de programas de computador Custos e análise de custo
• Palavra(s)-Chave do Pesquisador: Teste de Software | Verificação Formal | Métodos Formais

Resumo

Para que haja uma garantia de que o software desenvolvido é confiável, atividades de testes e verificação formal devem ser realizadas. Contudo, a viabilidade prática de execução dessas atividades depende de métodos de desenvolvimento que explorem o uso conjunto das técnicas, bem como de ferramentas que auxiliem sua realização, uma vez que a execução de ambas constitui um alto custo para o desenvolvimento do software. Tendo em vista a necessidade de facilitar a realização de testes e verificação formal nos sistemas de software de missão crítica, este projeto se propõe a desenvolver uma metodologia integrada, com apoio de ferramentas computacionais, para a verificação formal e testes desses sistemas, levando em conta a redução dos custos das atividades de Verificação e Validação (V&V). Os principais objetos de estudo que constituem um desafio científico ao projeto é a exploração da complementariedade das duas atividades de forma transversal ao desenvolvimento de sistemas críticos para possibilitar o uso conjunto dessas atividades e avaliar o custo de sua aplicação. (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. (13/22317-6, 12/23767-2, 11/01928-1)

DOS SANTOS, LUCIANA BRASIL REBELO; DE SANTIAGO, VALDIVINO ALEXANDRE JUNIOR; VIJAYKUMAR, NANDAMUDI LANKALAPALLI. Transformation of UML Behavioral Diagrams to Support Software Model Checking. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, v. N/A, n. 147, p. 10-pg., 2014-01-01. (12/23767-2)