Métodos formais

Na ciência da computação e engenharia de software, métodos formais são técnicas baseadas em formalismos matemáticos para a especificação, desenvolvimento e verificação dos sistemas de softwares e hardwares. Seu uso para o desenvolvimento de software e hardware é motivado pela expectativa de que, como em outras disciplinas de engenharia, possam contribuir para a confiabilidade e robustez de um projeto executando análises matemáticas apropriadas. Entretanto, o alto custo do uso dos métodos formais faz com que, de modo geral, sejam usados apenas no desenvolvimento de sistemas de alta-integridade, nos quais há alta probabilidade de as falhas provocarem perda de vidas ou sério prejuízo.

Taxonomia

Métodos formais podem ser empregados em diversos níveis:

Nível 0: Um sistema é descrito através de uma Especificação formal e essa especificação é usada como base para a implementação desse sistema. Denominado de método formal leve, em muitos casos é a opção de menor custo-benefício.

Nível 1: O Desenvolvimento e a verificação formal podem ser usados para produzir um programa de maneira mais formal. Por exemplo, as propriedades de um programa podem ser verificadas a partir de sua especificação, bem como o seu refinamento. Este método pode ser mais apropriado em sistemas de alta-integridade que envolvem segurança ou confiança.

Nível 2: Provadores de teoremas podem ser usados para conduzir testes completos das propriedades de um sistema de maneira automatizada. Este método pode se revelar muito dispendioso, sendo apenas vantajoso se o custo provocado pelos erros for extremamente alto (e.g., em partes críticas do projeto de um microprocessador).

Assim como a sub-disciplina de Semântica formal, os estilos dos métodos formais podem ser, em termos gerais, classificados como segue:

• Denotações semânticas: um sistema é expresso na teoria matemática de domínios. Os defensores desse método confiam na já bastante difundida natureza dos domínios para dar sentido ao sistema; os críticos argumentam que nem todo sistema pode ser intuitivamente ou naturalmente visto como uma função.
• Operações semânticas: um sistema é expresso como uma seqüência de ações de um modelo computacional (presumidamente) mais simples. Defensores desse método apontam para a simplicidade dos seus modelos como meio de expressar claridade; os críticos consideram que os problemas envolvendo semântica ainda não foram resolvidos (quem define a semântica de um modelo mais simples?).
• Axiomatizações semânticas: um sistema é expresso em termos de pré-condições e pós-condições que são verdadeiras antes e depois do sistema executar uma tarefa, respectivamente. Defensores apontam a conexão com a lógica clássica; os críticos dizem que tais semânticas nunca descrevem de fato o que um sistema faz (meramente o que é verdade antes e depois).

Métodos formais leves

Alguns especialistas acreditam que a comunidade de métodos formais tem sobrevalorizado a formalização completa de uma especificação ou projeto. Eles afirmam que a expressividade da linguagem envolvida, assim como a complexidade dos sistemas modelados, torna toda formalização uma tarefa difícil e dispendiosa. Como alternativa, foram propostos vários métodos formais leves, os quais enfatizam especificações parciais e aplicações focadas. Exemplos desta abordagem leve dos métodos formais incluem a Alloy object modelling notation, A síntese de Denney sobre alguns aspectos da notação Z com casos de uso orientado ao desenvolvimento, e as Ferramentas CSK VDM.

Usos

Métodos formais podem ser aplicados em vários pontos através do processo de desenvolvimento. (Por conveniência, nós usamos termos comuns para o modelo cascata, embora qualquer processo de desenvolvimento possa ser usado).

Especificação

Métodos formais podem ser usados para dar uma descrição do sistema a ser desenvolvido, em qualquer nível de detalhe desejado. Esta descrição formal pode orientar futuras atividades de desenvolvimento (veja seções seguintes); além disso, é possível empregá-la na verificação dos requerimentos de um sistema em desenvolvimento, e assim, atestar se foram completamente e precisamente especificados.

Por anos, sentiu-se a necessidade de sistemas de especificação formal. No relatório ALGOL 60, John Backus apresentou uma notação formal para a sintaxe de linguagens de programação descritivas (Mais tarde, nomeada de Forma Normal de Backus ou Forma Backus-Naur (BNF)). Backus também descreveu a necessidade para uma notação referente à semântica da linguagem de programação descritiva. O relatório previu que uma nova notação, tão definitiva como a BNF, iria aparecer em um futuro breve, porém isto nunca ocorreu.

Desenvolvimento

Uma vez descrita, a especificação formal pode ser usada como guia enquanto o sistema concreto é desenvolvido durante o processo de projeto (i.e. implementado tipicamente em software, mas potencialmente em hardware). Exemplos:

• Se a especificação formal está numa semântica operacional, o comportamento observado do sistema concreto pode ser comparado com o comportamento da especificação (a qual deve ser executável ou simulável). Adicionalmente, os comandos operacionais da especificação podem ser concebidos para a tradução direta em código executável.
• Se a especificação formal está numa semântica axiomática, as precondições e precondições da especificação podem se tornar afirmações no código executável.

Verificação

Uma vez desenvolvida, a especificação formal pode ser usada como base para a comprovação das propriedades da especificação (e, esperançosamente, por inferência, do sistema desenvolvido).

Prova Dirigida a Humanos

Às vezes, a motivação para provar a correção de um sistema não é a necessidade óbvia de reassegurar a correção do sistema, mas um desejo de entender melhor o sistema. Consequentemente, algumas provas de correção são produzidas no estilo de prova matemática: manuscritas (ou digitadas) usando linguagem natural, em um nível de informalidade comum a provas dessa categoria. Uma “boa” prova é uma que seja legível e inteligível por outros leitores humanos.

Críticos dessa abordagem afirmam que a ambiguidade inerente da linguagem natural leva a erros indetectáveis; frequentemente, erros sutis podem estar presentes em detalhes de baixo nível tipicamente negligenciados por essas provas. Adicionalmente, o trabalho envolvido em produzir uma boa prova requer um alto nível de sofisticação e especialização matemática.

Prova automatizada

Em contraste, há interesse crescente em produzir provas de correção de sistemas pelos meios automatizados. Técnicas automatizadas se enquadram em duas categorias gerais:

• Prova do teorema automatizado, na qual o sistema tenta produzir uma prova formal a partir do zero, dados uma descrição do sistema, um conjunto de axiomas lógicos, e um conjunto de regras de inferência.
• Verificação de Modelo, na qual o sistema verifica certas propriedades por meio de uma pesquisa exaustiva de todos os estados possíveis que um sistema poderia assumir durante sua execução.

Nenhuma dessas técnicas trabalha sem assistência humana. Provas de teoremas automatizadas normalmente requerem orientação sobre quais propriedades são “interessantes” o bastante para verificar; o verificador de modelos pode passar muito tempo conferindo milhões de estados desinteressantes se não tiver disponível um modelo suficientemente abstrato.

Proponentes desses sistemas argumentam que os resultados obtidos conferem maior certeza matemática do que provas produzidas pelo homem, uma vez que todos os detalhes tediosos são verificados por um algoritmo. O treinamento exigido para usar esses sistemas também é menor do que aquele exigido para produzir boas provas matemáticas manualmente, tornando as técnicas acessíveis para uma ampla variedade de especialistas.

Críticos notam que esses sistemas são como oráculos: eles fazem um pronunciamento da verdade, ainda que dê nenhuma explicação daquela verdade. Também há o problema do “verificando o verificador”; se o programa que ajuda na verificação não for provado, pode haver razões para duvidar da validade dos resultados obtidos.

Críticas

O campo dos métodos formais tem seus críticos. Provas de correção, manuscritas ou assistidas por computador, precisam de tempo significativo (e, portanto, de dinheiro) para serem produzidas, com utilidade limitada e voltadas apenas para assegurar a precisão. Por essa razão, os métodos formais são mais frequentemente usados em áreas onde os benefícios de se conseguir essas provas, ou o risco de haver erros não detectados, compensam os recursos empregados. Exemplo: na engenharia aeroespacial, erros não detectados podem causar mortes, portanto métodos formais são mais populares nesta área em comparação a outras.

Métodos formais e notações

Há uma variedade de métodos formais e notações disponíveis, incluindo:

• Máquina de estado abstrata (ASM)
• Alloy
• Método B
• Processo Calculi
  • Processo de comunicação sequencial (CSP)
  • π-calculus
• Modelo de Ator
• Esterel
• Lustre
• Rede de Petri
• RAISE
• Método de desenvolvimento Viena (VDM)
• Notação Z

Ver também

• Provador automático de teoremas
• Modelo de verificação
• Engenharia de software

Ligações externas

• Sociedade Brasileira de Computação (Página de Métodos Formais);
• Puc-RS;