Potencial Contributo da Verificação de Modelos para a Programação Genética

Abstract

A criação de modelos de sistemas concorrentes e distribuídos não é uma tarefa trivial. É necessária definir uma especificação sem falhas e um modelo que a satisfaça totalmente. Nos últimos anos foram estudadas várias abordagens que recorrem às técnicas Verificação de Modelos e Programação Genética, de forma a corrigir e melhorar código. Há questões por explorar, como a possibilidade de utilizar o resultado da verificação para evoluir modelos que satisfazem uma dada especificação. O objetivo desta dissertação consiste no estudo do potencial contributo da aplicação da Verificação de Modelos para auxiliar o processo evolucionário. Nomeadamente, incluir o tamanho dos contra-exemplos gerados na fase da verificação para o cálculo da aptidão de modelos. Efetuar a comparação da abordagem proposta com a criação aleatória e listagem exaustiva de modelos. A aplicação Formally Correct Genetic Programming foi o ambiente experimental que permitiu simular a evolução dos modelos (gerados com a ECJ) e avaliados com o verificador de modelos SPIN. Os resultados obtidos permitem comprovar que a abordagem proposta apenas é viável para problemas com um espaço de procura reduzido. Mostrou ser uma abordagem mais vantajosa que as restantes mencionadas. Os contra-exemplos de especificações incompletas ajudaram a desenvolver novas. Um elevado número de propriedades do tipo safety favoreceu a pesquisa de modelos. A verificação mostrou ser uma técnica demorada, questionando assim o seu uso para problemas mais complexos.

The creation of concurrent and distributed system models is not a trivial task. It is necessary to define a flawless specification and a model that fully satisfies it. In recent years, several approaches have been studied which resort to the techniques of Model Checking and Genetic Programming to correct and improve code. There are issues to explore, such as the possibility of using the verification result to evolve models that satisfy a given specification. The objective of this dissertation is to study the potential contribution of the application of the model verification to aid the evolutionary process. In particular, include the length of the counterexamples generated in the verification phase for the calculation of fitness models. Compare the proposed approach with the random creation and exhaustive listing of models. The application Formally Correct Genetic Programming was the experimental environment which allowed the simulation of the evolution of the models (generated with ECJ) and evaluated with the model checker SPIN. The results obtained allow to demonstrate that the proposed approach is only feasible for problems with a reduced search space. It has shown to be a more advantageous approach than the others mentioned. The counterexamples of incomplete specifications helped to develop newer ones. An elevated number of safety properties favored the search for solutions. The verification proved to be a lengthy technique, thus questioning its use for more complex problems.