Prof. Dr. Odorico Machado Mendizabal 

Universidade Federal do Rio Grande

Título: Verificação de Modelos com Spin

Resumo: Verificação de modelos é uma técnica utilizada para verificar algoritmos e sistemas computacionais. Uma ampla utilização desta técnica é observada na verificação de sistemas complexos, como sistemas concorrentes, distribuídos, tolerantes à falhas ou digitais. O processo de verificação consiste em modelagem, descrição de propriedades e verificação automática. Através de um formalismo de especificação é possível descrever o comportamentos do sistema na forma de um modelo. Propriedades desejáveis do modelo são comumente descritas em lógica temporal e verificadas pelo verificador, que explora o espaço de estados do modelo na busca por estados que violem as propriedades. Contra-exemplos gerados auxiliam a encontrar traços de execução que invalidam as propriedades do modelo. Este minicurso apresenta uma introdução sobre verificação de modelos, descrevendo um processo básico de verificação de modelos. Além disso, será introduzida a Lógica Linear Temporal e a descrição de propriedades usando lógica temporal. Exemplos práticos são apresentados com o uso da linguagem de especificação Promela e o verificador de modelos Spin.

Short bio: Odorico Machado Mendizabal é professor na Universidade Federal do Rio Grande (FURG). Obteve os títulos de Doutor e Mestre em Ciência da Computação pela Pontifícia Universidade Católica do Rio Grande do Sul e Engenharia de Computação pela Universidade Federal do Rio Grande. Antes de tornar-se professor, ele assumiu posições de desenvolvedor e analista de desempenho de software nas empresas HP e Dell. Suas áreas de interesse incluem sistemas distribuídos, tolerância a falhas, verificação e teste de software.