Propostas submetidas

DEI - FCTUC
Gerado a 2024-03-29 12:39:19 (Europe/Lisbon).
Voltar

Titulo Estágio

Programação Genética Verificada Formalmente

Áreas de especialidade

Engenharia de Software

Local do Estágio

DEI-FCTUC

Enquadramento

Esta proposta de tese tem como objetivo aplicar a Verificação de Modelos à Programação Genética. A Verificação de Modelos (Model Checking) é uma técnica muito eficaz para a verificação de software, particularmente interessante para verificar software concorrente e distribuído, tendo sido amplamente adotada pela indústria. Pretende-se aplicar, de forma automática, a verificação de modelos a programas gerados através de Programação Genética.

Os Algoritmos Evolutivos (como a Programação Genética) podem ser descritos como técnicas de pesquisa meta-heurística que utilizam a evolução simulada como estratégia de pesquisa; para este efeito, geram iterativamente populações de hipóteses de solução para um determinado problema, utilizando operadores inspirados em conceitos da genética e da seleção natural. A Programação Genética, em particular, visa a construção automática de programas computacionais que permitam executar uma tarefa especificada. Cada indivíduo da população (i.e., cada possível solução) é avaliado utilizando uma função de avaliação; o valor devolvido por esta função deve refletir a qualidade do indivíduo enquanto solução para o problema, e condicionar as probabilidade deste ser seleccionado para participar na constituição da geração seguinte.

As características dos Algoritmos Evolutivos (e da Programação Genética em particular) tornam-nos especialmente úteis para encontrar boas soluções para problemas de pesquisa e otimização utilizando baixos recursos computacionais; neste sentido, o estudo deverá focar-se em problemas reais, como sejam: semáforos em interseções, ordenação de arrays, n-queens, protocolos de consenso.

Objetivo

O principal objectivo será o de estudar o potencial de aplicar técnicas de Model Checking para auxiliar a guiar o processo de pesquisa, nomeadamente através da verificação formal de modelos gerados utilizando Programação Genética e da inclusão desta informação no cálculo da aptidão (fitness) de um indivíduo; determinada solução será tanto mais adequada quanto mais próxima estiver de atender à especificação do problema.

Pretende-se, neste sentido, que sejam exploradas abordagens que potenciem a utilização sinérgica de técnicas de Model Checking e de Programação Genética; e, especificamente, que sejam consideradas as características dos contra-exemplos gerados sempre que não seja possível verificar a correcção de determinado modelo (gerado por Programação Genética) para definir a aptidão do solução representada por esse modelo e para, consequentemente, guiar a pesquisa evolutiva.

Plano de Trabalhos - Semestre 1

- Estudo do estado da arte e levantamento de requisitos (mês 1)

A primeira fase consistirá em tomar contacto com conceitos de Model Checking e de Programação Genética, bem como na familiarização com os desafios existentes. Este processo deverá resultar numa clara formulação dos objectivos a alcançar.

- Familiarização com as ferramentas (mês 2)

Nesta fase o estudante deve-se-á familiarizar com as ferramentas relevantes, de entre as quais se deverão destacar as seguintes:
Spin: http://spinroot.com/spin/whatispin.html
ECJ: https://cs.gmu.edu/~eclab/projects/ecj/

- Aplicar a abordagem definida a problemas de benchmarking clássicos (meses 3 e 4)

Esta tarefa envolve a aplicação das técnicas e ferramentas estudadas a problemas de benchmarking clássicos, conduzindo experiências que permitam: identificar e quantificar os ganhos da aplicação de técnicas de Model Checking e Programação Genética de modo sinérgico; definir os parâmetros e configurações que se afigurem como os mais adequados; e delinear estratégias para aplicar a metodologia definida a problemas reais.

- Escrita de um technical report (mês 5)

O estudante deve documentar as tarefas efectuadas até este ponto e descrever o trabalho a realizar por via da escrita de um relatório intermédio e da preparação de uma apresentação pública para discussão.

Plano de Trabalhos - Semestre 2

- Desenho e implementação um case study baseado num problema real (meses 6 e 7)

Nesta fase deve aplicar-se a metodologia desenvolvida a um problema real (ou mais) a definir por a validar e estabelecer a pertinência da abordagem proposta. Devem ser conduzidas experiências que permitam obter métricas relativas ao desempenho.

- Avaliação dos mecanismos desenvolvidos (mês 8)

Esta tarefa consiste na avaliação da metodologia tendo por base, principalmente, as métricas obtidas na tarefa anterior. Adicionalmente, devem implementar-se (se necessário) e avaliar-se eventuais abordagens alternativas propostas na literatura por forma a permitir uma avaliação comparativa.

- Escrita do relatório final e artigo científico (mês 9).

O estudante deverá escrever uma tese descrevendo e discutindo o problema, a metodologia proposta, os resultados obtidos e tópicos para trabalho futuro; bem como preparar a sua apresentação e discussão pública. Paralelamente, deverá escrever um artigo científico com o objectivo de efectuar uma submissão para uma conferência de relevo na área.

Condições

O trabalho irá ser realizado no Departamento de Engenharia Informática da Universidade de Coimbra e será facultado o acesso a equipamento informático bem como aos laboratórios do DEI.

Observações

Nada a acrescentar.

Orientador

Raul Barbosa, José Ribeiro
rbarbosa@dei.uc.pt 📩