Pós-Graduação em Ciência da Computação – UFPE
Defesa de Dissertação de Mestrado Nº 1.934
Aluno: Thayonara de Pontes Alves
Orientador: Prof. Leopoldo Motta Teixeira
Título: Porting the Software Product Line Refinement Theory to the Coq
proof assistant: A Case Study
Data: 27/10/2020
Hora/Local: 9h – Virtual – https://meet.google.com/tmy-rsxh-soq
Banca Examinadora:
Prof. Gustavo Henrique Porto de Carvalho (UFPE / Centro de Informática)
Prof. Rohit Gheyi (UFCG / Departamento de Sistemas e Computação)
Prof. Leopoldo Motta Teixeira (UFPE / Centro de informática)
RESUMO:
Linhas de Produtos de Software (SPL em inglês) é uma abordagem para o desenvolvimento sistemático de produtos de software a partir de um conjunto de artefatos em comum. Melhoria da qualidade do produto, redução de custos de desenvolvimento e o rápido desenvolvimento de software têm sido os principais atrativos por trás dessa abordagem. No entanto, em cenários de evolução desses sistemas, é necessário que haja a garantia de que não estamos introduzindo erros ou alterando o comportamento dos produtos existentes. Através da teoria do refinamento da linha de produtos podemos assegurar uma evolução segura. Esta teoria foi especificada e comprovada usando o assistente de provas Prototype Verification System (PVS). No entanto, um outro assistente de prova, Coq, tem se tornado cada vez mais popular entre pesquisadores e desenvolvedores e, dado que algumas linguagens de programação já estão formalizadas em tal ferramenta, a teoria do refinamento pode se beneficiar do potencial de integração. Dessa forma, neste trabalho, apresentamos um estudo de caso sobre a portabilidade da especificação PVS da teoria de refinamentos para Coq. Esta especificação inclui modelos específicos, tais como Feature Model, Asset Mapping e Configuration Knowlegde, como também a instanciação usando Typeclasses, além da formalização de templates que podem ser usados em cenários de evolução de SPL. Adicionalmente, pelo fato dessa teoria já ter sido formalizada no PVS, comparamos os assistentes de prova com base nas diferenças observadas entre as especificações e as provas dessa teoria, proporcionando algumas reflexões sobre as táticas e estratégias utilizadas para compor as provas. Como resultado, de acordo com nosso estudo, o PVS forneceu definições mais sucintas do que o Coq, em vários casos, bem como um maior número de comandos automáticos bem-sucedidos que resultaram em provas mais curtas. Apesar disso, Coq também trouxe facilidades nas definições, como tipos enumerados e recursivos, e recursos que dão suporte aos desenvolvedores em suas provas.
Palavras-chave: Software product lines. Theorem provers. Coq. PVS.
Comentários desativados