LÓGICA TEMPORAL PARA VERIFICAÇÃO DE PROGRAMAS

Resumo

Existe uma grande vantagem em ser capaz de verificar a correção de sistemas computacionais, sejam eles de hardware, de software ou uma combinação dos dois. Métodos de verificação formal tornaram-se utilizáveis pela indústria e existe uma demanda crescente de profissionais capazes de aplicá-los. O objetivo deste trabalho é aplicar lógicas modais temporais para fazer a verificação automática de sistemas, através de suas propriedades, fazendo testes com os mais variados exemplos e problemas da computação. Como metodologia, foi estudado três tipos de lógicas temporais: LTL (Lógica Temporal de Tempo Linear); CTL (Lógica de Árvore Computacional); CTL* (uma lógica que combina os poderes de expressão da LTL e CTL), e também utilizou-se o programa NuSMV (Novo Verificador de Modelos Simbólico) para fazer aplicações práticas de verificação. A ideia da lógica temporal é que uma fórmula não é estaticamente verdadeira ou falsa em um modelo, como em outras lógicas. Seus modelos contêm diversos estados, e uma fórmula pode ser verdadeira em alguns estados e falsa em outros. Na verificação, os modelos são sistemas de transição e as propriedades são fórmulas em lógica temporal. O NuSMV fornece uma linguagem para descrever os modelos e verifica diretamente a validade de fórmulas da LTL e CTL. Como resultados, foram realizados testes com vários exemplos que funcionaram perfeitamente em relação à verificação. Constatou-se que LTL e CTL tem diferentes poderes expressivos: LTL permite selecionar um intervalo de caminhos, enquanto que CTL permite fazer uma quantificação explícita por caminhos. Conclui-se que a lógica CTL* surge como uma alternativa para ganhar mais expressividade, porém perdendo na complexidade, combinando as duas lógicas anteriores e estendendo-as. Essa abordagem se mostrou muito eficiente e promissora em relação à verificação de programas. Agradeço ao CNPq pela oportunidade de ser bolsista de Iniciação Científica.