Verificação de Modelo: diferenças entre revisões
m Bot: Modificando: sk:Overovanie modelov; mudanças triviais |
|||
| Linha 1: | Linha 1: | ||
{{sem-fontes|data=Abril de 2009}} |
|||
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. |
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 [[protocolo de comunicação|protocolos de comunicação]] e suas especificações contém |
Tipicamente estes são sistemas de [[hardware]], [[software]] e [[protocolo de comunicação|protocolos de comunicação]] e suas especificações contém requisitos de segurança como a ausência de [[deadlock]]s e comportamentos similares que podem levar o sistema a [[Crash (informática)|falhar]]. 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== |
|||
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. Emerson]]<ref name=Allen1980>{{citation |
|||
| last1 = Allen Emerson | first1 = E. |
|||
| last2 = Clarke | first2 = Edmund M. |
|||
| year = 1980 |
|||
| title = Characterizing correctness properties of parallel programs using fixpoints |
|||
| journal = Automata, Languages and Programming |
|||
| doi = 10.1007/3-540-10003-2_69 |
|||
}}</ref><ref name="LoP81">Edmund M. Clarke, E. Allen Emerson: [http://portal.acm.org/citation.cfm?id=747438&dl= "Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic"]. Logic of Programs 1981: 52-71.</ref><ref name=Clarke1986>{{citation |
|||
| last1 = Clarke | first1 = E. M. |
|||
| last2 = Emerson | first2 = E. A. |
|||
| last3 = Sistla | first3 = A. P. |
|||
| year = 1986 |
|||
| title = Automatic verification of finite-state concurrent systems using temporal logic specifications |
|||
| journal = ACM Transactions on Programming Languages and Systems |
|||
| volume = 8 |
|||
| pages = 244 |
|||
| doi = 10.1145/5397.5399 |
|||
}}</ref> and by J. P. Queille and [[J. Sifakis]]<ref name=Queille1982>{{citation |
|||
| last1 = Queille | first1 = J. P. |
|||
| last2 = Sifakis | first2 = J. |
|||
| year = 1982 |
|||
| title = Specification and verification of concurrent systems in CESAR |
|||
| journal = International Symposium on Programming |
|||
| doi = 10.1007/3-540-11494-7_22 |
|||
}}</ref>. 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 <math>M,s \models p</math> . Se M é finito, como é em hardware, a verificação de modelos se reduz a uma busca gráfica. |
|||
==References== |
|||
{{reflist}} |
|||
{{esboço-informática}} |
{{esboço-informática}} |
||
Revisão das 16h34min de 6 de novembro de 2009
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 falhar. 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
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. Emerson[1][2][3] and by J. P. Queille and J. Sifakis[4]. 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 . Se M é finito, como é em hardware, a verificação de modelos se reduz a uma busca gráfica.
References
- ↑ 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
- ↑ Edmund M. Clarke, E. Allen Emerson: "Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic". Logic of Programs 1981: 52-71.
- ↑ 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
- ↑ 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
