Titulo Estágio
Programação genética verificada formalmente
Áreas de especialidade
Engenharia de Software
Sistemas Inteligentes
Local do Estágio
Departamento de Engenharia Informática
Enquadramento
Esta dissertação 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 objetivo 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 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 do relatório intermédio (mês 5)
As tarefas realizadas no decorrer do primeiro semestre devem ser documentadas na forma de um relatório intermédio, seguindo-se a sua apresentação pública e discussão. Será importante apresentar nesse relatório os resultados obtidos no primeiro semestre.
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 (meses 8 e 9)
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 da dissertação de mestrado (mês 10)
Deve ser concluída a escrita da dissertação de mestrado e preparada a respetiva apresentação pública. A dissertação deve documentar todo o trabalho realizado, os resultados e as conclusões obtidas. Se os resultados forem promissores será recomendada a escrita de um artigo científico.
Condições
O trabalho irá ser realizado no Departamento de Engenharia Informática da Universidade de Coimbra e o/a estudante terá acesso a um local de trabalho nos laboratórios do DEI bem como ao equipamento informático necessário.
Observações
Esta dissertação irá beneficiar da colaboração e co-orientação do Dr. José Ribeiro do Instituto Politécnico de Leiria.
Orientador
Raul Barbosa
rbarbosa@dei.uc.pt 📩