Detalhes bibliográficos
| Ano de defesa: |
2017 |
| Autor(a) principal: |
Hora, Bruno Vercelino da |
| Orientador(a): |
Não Informado pela instituição |
| Banca de defesa: |
Não Informado pela instituição |
| Tipo de documento: |
Dissertação
|
| Tipo de acesso: |
Acesso aberto |
| Idioma: |
por |
| Instituição de defesa: |
Biblioteca Digitais de Teses e Dissertações da USP
|
| Programa de Pós-Graduação: |
Não Informado pela instituição
|
| Departamento: |
Não Informado pela instituição
|
| País: |
Não Informado pela instituição
|
| Palavras-chave em Português: |
|
| Link de acesso: |
http://www.teses.usp.br/teses/disponiveis/45/45134/tde-02102017-114414/
|
Resumo: |
Uma importante etapa do desenvolvimento de software é o de levantamento e análise dos requisitos. Porém, durante esta etapa podem ocorrer inconsistências que prejudicarão o andamento do projeto. Além disso, após finalizada a especificação, o cliente pode querer acrescentar ou modificar as funcionalidades do sistema. Tudo isso requer que a especificação do software seja revista, mas isso é altamente custoso, tornando necessário um processo automatizado para simplificar tal revisão. Para lidar com este problema, uma das abordagens utilizadas tem sido o processo de Revisão de Crenças, juntamente com o processo de Verificação de Modelos. O objetivo deste trabalho é utilizar o processo de revisão de crenças e verificação de modelos para avaliar especificações de um projeto procurando inconsistências, utilizando o fragmento universal da Computation Tree Logic (CTL), conhecido como ACTL, e revisá-las gerando sugestões de mudanças na especificação. A nossa proposta é traduzir para lógica clássica tanto o modelo (especificação do software) quanto a propriedade a ser revisada, e então aplicar um resolvedor SAT para verificar a satisfazibilidade da fórmula gerada. A partir da resposta do resolvedor SAT, iremos gerar sugestões válidas de mudanças para a especificação, fazendo o processo de tradução reversa da lógica clássica para o modelo original. |
