Banca de QUALIFICAÇÃO: ERNESTO CID BRASIL DE MATOS

Uma banca de QUALIFICAÇÃO de DOUTORADO foi cadastrada pelo programa.
DISCENTE: ERNESTO CID BRASIL DE MATOS
DATA: 13/08/2015
HORA: 09:00
LOCAL: sala de reuniões do DIMAp
TÍTULO:

BETA: uma Abordagem de Testes Baseada em B


PALAVRAS-CHAVES:

Testes, Métodos Formais, Método B, Testes baseados em modelos formais


PÁGINAS: 95
GRANDE ÁREA: Ciências Exatas e da Terra
ÁREA: Ciência da Computação
SUBÁREA: Metodologia e Técnicas da Computação
ESPECIALIDADE: Engenharia de Software
RESUMO:

Sistemas de software estão presentes em grande parte das nossas vidas atualmente e, mais do que nunca, eles requerem um alto nível de segurança e confiabilidade. No mundo do desenvolvimento de software existem várias técnicas de Verificação e Validação (V&V) que se preocupam com controle de qualidade, segurança, robustez e confiabilidade; dentre as mais conhecidas temos Testes de Software e Métodos Formais. Métodos formais e testes são técnicas que podem se complementar. Enquanto métodos formais provêem mecanismos confiáveis para raciocinar sobre o sistema em um nível mais abstrato, técnicas de teste ainda são necessárias para uma validação mais profunda e são frequentemente requeridas por orgãos de certificação. Nesta proposta de tese de doutorado nós propomos uma abordagem suportada por ferramenta para gerar casos de teste a partir de máquinas abstratas do Método B. O Método B é um método formal que usa conceitos de Lógica de Primeira Ordem, Teoria dos Conjuntos e Aritmética Inteira para especificar máquinas de estado abstratas que modelam o comportamento de componentes de um sistema. A abordagem proposta utiliza propriedades especificadas nestes modelos e aplica técnicas de teste bem fundamentadas pela comunidade de testes, como particionamento do espaço de entrada e critérios de cobertura lógica, para gerar casos de teste para a implementação do sistema. Os casos de teste gerados são testes de unidade que verificam se o código desenvolvido implementa o comportamento especificado nos modelos abstratos. Os requisitos para cada caso de teste são definidos usando fórmulas lógicas que são passadas como entrada para um solucionador de restrições para obter dados de teste. A ferramenta também provê funcionalidades para o cálculo de preâmbulos, verificação de oráculos e concretização dos dados de teste. Ela é capaz de gerar especificações de casos de teste e scripts de teste executáveis escritos em Java e C. A abordagem foi avaliada através de vários estudos de caso – utilizando modelos simples e complexos – e mostrou resultados promissores, sendo capaz de identificar defeitos inseridos durante o processo de refinamento e codificação, e defeitos criados por geradores de código defeituosos.


MEMBROS DA BANCA:
Presidente - 1258224 - ANAMARIA MARTINS MOREIRA
Interno - 2220777 - DAVID BORIS PAUL DEHARBE
Externo à Instituição - PATRICIA DUARTE DE LIMA MACHADO - UFCG
Notícia cadastrada em: 14/07/2015 16:00
SIGAA | Superintendência de Informática - (84) 3215-3148 | Copyright © 2006-2017 - UFRN - sigaa04-producao.info.ufrn.br.sigaa04-producao