Verificação formal

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa

Verificação formal é a prova matemática da conformidade dum algoritmo a certa especificação formal ou propriedade, usando métodos formais.

Uso[editar | editar código-fonte]

A verificação formal pode ser usado em sistemas como protocolos de criptografia, circuitos combinatórios, circuitos digitais com memória interna e programas de computador expressados através de código fonte. A verificação desses sistemas é feita fornecendo uma prova matemática num modelo matemático abstrato do sistema, a correspondência entre o modelo matemático e a natureza do sistema conhecido por construção. Exemplos de estruturas usadas para modelar sistemas incluem máquinas de estado finito, redes de Petri, além de semânticas formais como operacional, denotacional, axiomática e a lógica de Hoare.

Abordagens[editar | editar código-fonte]

Existem basicamente duas abordagens para a verificação formal.

A primeira é a verificação de modelos, que consiste numa exploração sistematicamente exaustiva do modelo matemático, o que é possível para modelos finitos, mas também para modelos infinitos em que conjuntos finitos de estados podem ser representados. Isso geralmente consiste na exploração de todos os estados e transições do modelo, ao usar técnicas de abstração para considerar grupos de estados numa única operação, reduzindo o tempo de processamento.

A segunda abordagem é a inferência lógica, que consiste na utilização duma formalização matemático do sistema, através do uso de software de prova de teoremas. Esse processo é geralmente automatizado parcialmente, dependendo do entendimento manual do sistema para a validação.

Ver também[editar | editar código-fonte]