Verificação de modelos

Origem: Wikipédia, a enciclopédia livre.
(Redirecionado de Model Checking)
Ir para: navegação, pesquisa

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 checar 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[editar | editar código-fonte]

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 E. M. Clarke and E. A. Emerson1 2 3 and by J. P. Queille and J. Sifakis4 . Clarke, Emerson e Sifakis receberam juntos o Turing Award 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 M,s \models p . Se M é finito, como é em hardware, a verificação de modelos se reduz a uma busca gráfica.

References[editar | editar código-fonte]

  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: 244, 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 


Ícone de esboço Este artigo sobre Informática é um esboço. Você pode ajudar a Wikipédia expandindo-o.