Voltar

Pós em Ciência da Computação realiza defesa de dissertação amanhã (27)

A defesa será realizada às 9h via Google Meet

O Programa de Pós-Graduação em Ciência da Computação, do Centro de Informática (CIn) da UFPE, realiza amanhã (27) a defesa da dissertação “Porting the Software Product Line Refinement Theory to the Coq proof assistant: A Case Study”. O trabalho, desenvolvido pela discente Thayonara de Pontes Alves e orientado pelo professor Leopoldo Motta Teixeira, será defendido às 9h, via Google Meet. A banca examinadora será composta pelo orientador e pelos professores Gustavo Henrique Porto de Carvalho (Centro de Informática/ UFPE) e Rohit Gheyi (Departamento de Sistemas e Computação/ UFCG).

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.

 

Data da última modificação: 26/10/2020, 18:12