Verificação de modelos

No campo da ciência da computação, verificação de modelos (do inglês, Model Checking) refere-se ao problema de testar automaticamente se um modelo que representa um sistema atende a uma dada especificação.

Tipicamente estes são sistemas de hardware, software e protocolos de comunicação e suas especificações contém requisitos de segurança como a ausência de deadlocks e comportamentos similares que podem levar o sistema a travar. Esse deadlock é uma situação onde duas ou mais ações simultaneamente esperam a finalização da outra para sua continuação, e assim nenhuma delas pode ser concluída.

Para resolver tal problema de maneira algorítmica, tanto o modelo do sistema quanto a especificação são formulados em alguma linguagem matematicamente precisa. Para esta finalidade, ela deve ser formulada como uma tarefa de lógica, de forma a verificar se uma dada estrutura satisfaz uma dada fórmula lógica. O conceito é geral e se aplica a todos os tipos de lógicas e estruturas apropriadas. Um problema simples de verificação de modelo é verificar se uma dada fórmula na lógica proposicional é satisfeita por uma dada estrutura.

Visão geral

Uma importante classe de métodos de verificação de modelos tem sido desenvolvida para verificação de modelos de projetos de hardware e software onde a especificação é dada por uma fórmula de lógica temporal. Trabalhos pioneiros em verificação de modelos de fórmula de lógica temporal foram realizados por Edmund Clarke e Ernest Allen Emerson^[1][2][3] e por J. P. Queille e Joseph Sifakis^[4]. Clarke, Emerson e Sifakis receberam juntos o Prêmio Turing de 2007 por seu trabalho em verificação de modelos.

Verificação de modelos é mais freqüentemente aplicada em projetos de hardware. Para software, devido à indecidabilidade, a abordagem não pode ser totalmente algorítmica; tipicamente ela pode provar ou não provar uma dada propriedade.

A estrutura é usualmente dada como descrição de código fonte numa linguagem descritiva industrial de hardware ou uma linguagem de propósito especial. Tal programa corresponde a uma máquina de estados finitos, ou seja, um dígrafo (ou quiver) consistindo de nós (ou vértices) e bordas. Um conjunto de proposições atomizadas está associada a cada nó, tipicamente estabelecendo quais elementos de memória são um nó. Os nós representam estados do sistema, as bordas representam possíveis transições que podem alterar o estado, enquanto que as proposições atomizadas representam as propriedades básicas que se mantém num ponto de execução.

Formalmente, o problema pode ser estabelecido da seguinte maneira: dada uma propriedade desejada, expressa como uma lógica temporal p, e uma estrutura M com estado inicial s, decida se ${\displaystyle M,s\models p}$ . Se M é finito, como é em hardware, a verificação de modelos se reduz a uma busca gráfica.

Referências

1. Allen Emerson, E.; Clarke, Edmund M. (1980), «Characterizing correctness properties of parallel programs using fixpoints», Automata, Languages and Programming, doi:10.1007/3-540-10003-2_69
2. Edmund M. Clarke, E. Allen Emerson: "Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic". Logic of Programs 1981: 52-71.
3. Clarke, E. M.; Emerson, E. A.; Sistla, A. P. (1986), «Automatic verification of finite-state concurrent systems using temporal logic specifications», ACM Transactions on Programming Languages and Systems, 8, doi:10.1145/5397.5399
4. Queille, J. P.; Sifakis, J. (1982), «Specification and verification of concurrent systems in CESAR», International Symposium on Programming, doi:10.1007/3-540-11494-7_22

Este artigo sobre informática é um esboço. Você pode ajudar a Wikipédia expandindo-o. v d e