Métodos formais

Origem: Wikipédia, a enciclopédia livre.

Esta página ou secção foi marcada para revisão, devido a inconsistências e dados de confiabilidade duvidosa. Se tem algum conhecimento sobre o tema, por favor verifique e melhore a consistência e o rigor deste artigo. Considere utilizar {{revisão-sobre}} para associar este artigo com um WikiProjeto.

Esta página precisa ser reciclada de acordo com o livro de estilo. Sinta-se livre para editá-la para que esta possa atingir um nível de qualidade superior.

Vivemos em um mundo computacional no qual vários problemas como a complexidade crescente nos sistemas; sistemas críticos envolvendo vidas e dinheiro; a necessidade de construção de sistemas confiáveis, e ambigüidade das especificações informais, urgem solução. Uma questão fundamental no desenvolvimento de um software é garantir que a "solução " encontrada realmente resolva o problema proposto, e é exatamente aí, onde entram os métodos formais.

Índice 1 O que são métodos formais? 1.1 Sete mitos dos métodos formais 2 Etapas do desenvolvimento de um sistema usando métodos formais 2.1 Especificação formal 2.1.1 Métodos formais leves 2.1.2 Classificação de especificação formal 2.2 Desenvolvimento de software 2.3 Verificação 2.3.1 Provadores de teoremas 2.3.1.1 Prova Humana-Dirigida 2.3.1.2 Prova Automatizada 3 Críticas 4 Métodos formais no Brasil 5 Vale a pena utilizar métodos formais? E se não utilizarmos? O que poderia acontecer? 6 Veja também e aumente a Wikipedia! 7 Veja também, em português 8 Conclusão 9 Referências 10 Ligações externas

[editar] O que são métodos formais?

^[1][2][3]

Métodos formais, na ciência da computação e engenharia de software, são técnicas matemáticas para o desenvolvimento e especificação dos sistemas de software e hardware. Para realizar tal tarefa no desenvolvimento, deve-se primeiro construir um modelo de solução especificada formalmente, utilizando uma linguagem formal. Tendo este modelo formal como base, pode-se ter os seguintes benefícios:

• Permitir que dúvidas sobre o projeto possam ser respondidas por avaliações matemáticas (prova de teorema ou verificação de modelo). Estas avaliações puramente simbólicas e precisas podem ser usadas para “debugging” e inspeção do projeto, bem como para verificação do software;
• Uso de linguagens técnicas e ferramentas, baseadas na lógica e matemática discreta, para especificação de software e verificação de sistemas, criando um sistema compreensivo e robusto de desempenho aceitável;
• A redução da dependência da intuição e julgamento humanos;
• Grande poder de abstração;
• Provar que o código está correto ao se realizar a implementação do desenvolvimento de software,
• Validar o modelo através de simulações e assim detectar inconsistências e ambigüidades na especificação decorrentes da "linguagem informal".

Como nem tudo na vida são flores, encontramos as seguintes desvantagens nos métodos formais:

Esse objetivo torna-se ainda mais imperativo quando software é empregado em sistemas cuja falha operacional pode ocasionar perdas humanas, econômicas ou causar degradação na prestação de serviços. Em ambientes críticos envolvendo sistemas de controle de tráfego aéreo ou de comando e controle de aeronaves, há uma necessidade preeminente de que os requisitos do sistema sejam precisamente especificados, objetivando implementar corretamente o projeto. Situação similar ocorre em sistemas sujeitos a sofrer degradação no nível de prestação de serviços quando operando em situação de falha. Exemplos de tais sistemas compreendem os sistemas de telecomunicações e sistemas de bancos com caixa de auto-atendimento.

• Em geral, o alto custo do uso de métodos formais, durante o desenvolvimento, levam-nos levam a serem aplicados apenas em sistemas de alta-integridade onde há alta probabilidade de falhas coduzirem a morte e/ou prejuízo.

[editar] Sete mitos dos métodos formais

^[4][5]

• 1. Métodos formais podem garantir um programa perfeito

Não é possível garantir a perfeição de nenhum programa, independentemente do método utilizado. Mesmo usando métodos formais, podem existir várias fases do projeto onde surgem imperfeições devido a existência de especificações que não são provadas. O ponto principal é que os benefícios de uma especificação formal são atingidos independentemente da garantia de sucesso do sistema.

• 2. Métodos formais só servem para provar que o programa é correto

O uso dos métodos formais vai além da prova. A parte mais importante do formalismo é a elaboração da especificação. A prova e verificação do programa associada ao método formal é a parte geralmente mais difícil do método, mas não a única que traz benefícios. Existem outros benefícios como a clarificação dos requisitos; a detecção de erros latentes e ambíguos, e as decisões sobre funcionalidades.

• 3. Somente sistemas de missão crítica são beneficiados pelo uso de métodos formais

Métodos formais são aplicáveis a qualquer projeto, e a melhora na especificação será refletida em um projeto executado de forma mais eficiente. Sistemas de missão crítica se beneficiam diretamente pela parte de verificação do método, mas todos os projetos se beneficiam de um documento de requisitos melhor elaborado.

• 4. Métodos formais envolvem matemática complexa

A matemática usada não é muito difícil, e consegue ser mais fácil do que a própria linguagem de programação. Usar qualquer ferramenta de computação requer algum aprendizado; a notação formal não deve fugir à regra. Usar treinamento e consultoria em matemática discreta e na notação formal pode suavizar a curva de aprendizado.

• 5. Métodos formais aumentam o custo do desenvolvimento

Na realidade, o uso de um método formal ajuda a especificar melhor o produto, e por isso, tende a encurtar o tempo total de implementação. Realmente passa-se mais tempo detalhando a especificação e menos programando. Durante a fase inicial é menos custoso consertar problemas, logo é importante não ter pressa neste momento. Como exemplo, a Rolls Royce relatou que em projetos de segurança onde foi usado especificações formais, se teve maior produtividade e evitaram grandes custos na parte final do projeto.

• 6. Métodos formais são incompreensíveis aos usúarios

A especificação formal ajuda a capturar corretamente o verdadeiro desejo do usuário, e por isso o beneficia diretamente. Para que o usuário entenda o progresso que está sendo feito, no entanto, é importante que se escreva paralelamente um documento em linguagem natural equivalente as especificações matemáticas.

• 7. Ninguém usa métodos formais em projetos reais

Métodos formais estão sendo usados em diversos projetos, em várias empresas diferentes. Exemplos que podemos citar são a IBM, no sistema CICS; a Tektronix, na especificação da funcionalidade de osciloscópios, e a Praxis.

[editar] Etapas do desenvolvimento de um sistema usando métodos formais

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

[editar] Especificação formal

^[6]

A especificação formal consiste numa fase onde se formaliza aspectos relevantes da aplicação e ambiente. Os desenvolvedores utilizam técnicas de especificação que ofereçam suporte, denominadas pelos mesmos como "5 C’s", que são: corretude, completude, consistência, concisão e clareza. A linguagem formal utilizada é uma coleção de símbolos extraídos de um alfabeto e um conjunto de regras sintáticas que regem as expressões baseadas em estado ou álgebra de processos. Todo este formalismo durante a especificação, permite a eliminação de ambigüidade, inconsistência às quais apenas seriam detectadas durante as fases de implementação e teste do ciclo de desenvolvimento de um sistema, resultando em menores gastos e menor possibilidade de falha no projeto. Tendo essa etapa realizada com sucesso, torna-se possível explorar o projeto de modo mais preciso e rigoroso, bem como verificar as propriedades das especificações do projeto e ainda analisar, de maneira sistemática, o comportamento do sistema antes de produzir o software. A necessidade de sistemas de especificação formal foi percebida durante anos. Porém, somente 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-Naur (BNF). Backus também descreveu a necessidade para uma notação referente a semântica da linguagem de programação descritiva. O relatório prometeu uma nova notação, tão definitiva como as BNF, num futuro muito breve.

[editar] Métodos formais leves

^{[7][8][9][10][11]}

Alguns especialistas acreditam que a comunidade de métodos formais tem se super enfatizado na formalização total da especificação ou design. Vários afirmam que a expressividade da linguagem envolvida, assim como a complexidade dos sistemas que estão atualmente sendo modelados, torna toda formalização uma tarefa muito mais difícil e cara. Buscando uma solução custo-eficiência, estes especialistas criaram certos tipos de especificações formais que podem ser empreendidas e então desenvolvidas de modo informal num programa. Esta ação alternativa está sendo chamada de métodos formais leves, que enfatizam especificações parciais e aplicações focadas. Entre os vários métodos de especificação formal leves pode-se citar a síntese de Daniel Jackson do MIT sobre modelagem de objetos em Alloy, que foi aplicada sobre vários aspectos da notação Z e utilizada em várias aplicações práticas com alguns casos de uso, conduziram ao desenvolvimento com sucesso. Também pode-se citar o método de gramática de grafos, por possuir uma linguagem visual de representação e descrever com naturalidade fenômenos de sistemas concorrentes e as ferramentas do CSK group que são os Métodos de Densenvolvimento Vienna(VDM).

[editar] Classificação de especificação formal

• Semântica denotacional, a qual o sentido de todo sistema é expresso na teoria matemática do domínio. Proponentes de tais métodos dependem da natureza do bom-entendimento do domínio para dar sentido ao sistema. Críticos mostram que nem todo sistema pode ser intuitivamente ou naturalmente visto como uma função.
• Operações semânticas, as quais o sentido do sistema é expresso como uma seqüência de ações de um (presumidamente) modelo computacional mais simples. Proponentes de tais métodos apontam para a simplicidade dos seus modelos como meio de expressar claridade. Críticos contam que os problemas de semântica acabam de ser atrasados devido a inexistência de alguém capaz de definir a semântica de um modelo mais simples.
• Axiomatizações semânticas, as quais o sentido do 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. Proponentes apontam a conexão com a lógica clássica. Críticos apontam que tais semânticas nunca descrevem o que um sistema realmente "faz" (meramente o que é verdade antes e subseqüentemente).

[editar] Desenvolvimento de software

Tendo um programa especificado formalmente, o desenvolvimento do sistema será mais preciso, robusto e compreensivo. Esta etapa, será influenciada pela formalização de provas e propriedades, levando ao refinamento da especificação de um sistema. Sabendo-se disso, o programa pode ser empreendido de melhor forma, logo, melhor desenvolvido. Isto será de alta prioridade e importância para sistemas de alta-integridade envolvendo segurança ou confiança.

Deve-se fazer o uso da especificação formal como guia até que o sistema concreto seja completamente desenvolvido (i.e. a realização completa entre todas as ligações entre softwares e/ou hardwares). Exemplos de abordagens:

• Se a especificação formal está numa semântica denotacional, o comportamento observado do sistema concreto restringem-se as verdades matemáticas referentes ao domínio formalizado.
• 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 (na qual deveria ser executável ou simulabilizável). Adicionalmente, os comandos operacionais da especificação podem ser amenizados ao direcionar a tradução em código executável.
• Se a especificação formal está numa semântica axiomática, as pré-condições e pós-condições da especificação podem tornar-se asserções no código executável.

[editar] Verificação

Uma vez que uma especificação formal tenha sido desenvolvida, a especificação pode ser usada como fundamento para propriedades de prova da implementação (e esperançosamente do sistema desenvolvido) no o uso de provadores de teoremas.

[editar] Provadores de teoremas

Os provadores de teoremas são meios para provar as especificações desenvolvidas no sistema, em lógica de primeira ordem, derivando-as ao se utilizar os métodos de resolução. Os provadores de teorema podem ser usados para verificar que um sistema particular apresenta uma propriedade específica, pois esta é uma atividade complexa, que envolve o tratamento de especificações complexas, muitos passos de inferência e a gerência de muitas informações. Isto pode ser muito caro e será vantajoso apenas se o custo de erros for extremamente alto. Os estilos de verificação dos métodos formais podem ser groseiramente classificados como segue:

[editar] Prova Humana-Dirigida

Algumas provas de correção são produzidas no estilo de prova matemática: manuscritas (ou compostas) usando linguagem natural, usando um nível de informalidade comum a tais provas. Uma “boa” prova é uma a qual seja legível e compreendida por outros leitores humanos. Em geral, se segue este escopo:

• Escolhe-se pontos chaves do programa;
• Identificam-se propriedades que devem ser satisfeitas naquele ponto do programa.
• Prova-se que tais propriedades são satisfeitas pelo programa
• Prova-se que a corretude do programa é uma consequência lógica da validade dos invariantes.

Críticos de tais aproximações mostram que a ambigüidade inerente na linguagem natural permite que erros não sejam detectados em tais provas. Freqüentemente, erros sutis podem estar presentes em detalhes de baixo nível, tipicamente negligenciados por tais provas. Adicionalmente, o trabalho envolvido em produzir tal boa prova requer um alto nível de sofisticação e especialização matemática.

[editar] Prova Automatizada

Em contraste, há interesse crescente pela massa científica em produzir provas de correção de tais sistemas por meios automatizados. Técnicas automatizadas entram em duas categorias gerais:

• Provador de teoremas automatizado, a qual o sistema tenta produzir uma prova formal com muita dificuldade, dando uma descrição do sistema, um conjunto de axiomas lógicos, e um conjunto de regras de inferência.
• Verificação de modelos, a qual o sistema verifica certas propriedades através de meios de uma pesquisa exaustiva de todos os estados possíveis que um sistema poderia entrar 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 prosseguir. O verificador de modelos pode muito facilmente “entrar em loop infinito” conferindo milhões de estados desinteressantes se não for dado um modelo abstrato suficiente. Proponentes de tais sistemas discutem que os resultados têm maior certeza matemática do que provas produzidas pelo homem, desde que todos os detalhes tediosos foram algoritimicamente verificados. O treinamento exigido para usar tais sistemas também é menor do que aquele exigido para produzir boas provas matemáticas manualmente, fazendo as técnicas acessíveis para uma ampla variedade de especialistas. Embora seja uma técnica poderosa, ainda é pouco prática e existe muita pesquisa para simplificar sua utilização. Os críticos notam que tais sistemas como estes, chamados de [Máquinas oráculos|máquinas oráculos], fazem um pronunciamento da verdade, ainda que não dêem nenhuma explicação daquela verdade. Também há o problema da "recursão de verificar o verificador". Se o programa que ajuda na verificação não for provado, existem várias razões para duvidar da validade dos resultados obtidos.

[editar] Críticas

Além das críticas internas mencionadas acima, o campo de métodos formais tem seus críticos unidos como um todo. No estado atual da arte, provas de correção sendo manuscritas ou assistidas por computador, precisam de tempo significante (e assim dinheiro) para produzir com utilidade limitada, ao invés de assegurar a precisão. Isto faz com que os métodos formais sejam mais propícios a serem usados em campos onde os benefícios de ter tais provas, ou o perigo em ter erros não detectados, fazem os recursos serem valorizados. Às vezes, proponentes de métodos formais têm reivindicado que as técnicas deles sejam consideradas a bala prateada que matará o último dos vampiros na Crise do software. Certamente, se acredita vastamente que não há nenhuma bala prateada para tal feito quanto ao desenvolvimento de software, e alguns até escrevem contra os métodos formais devido a tal exagero, extrapolando todas as reivindicações.

[editar] Métodos formais no Brasil

No Brasil, tem-se uma crescente pesquisa na área de métodos formais. Eis alguns exemplos:

• Especificação e verificação dos network wireless baseados nos protocolos do IEEE 802.11;
• Verificadores de modelo e verificadores formais;
• Especificações em CSP com diagramas UML-RT;
• Cálculo π baseada em tipos;
• Cálculo de complexidades de pior, melhor e caso médio de algoritmos recursivos;
• Especificações descritas em gramáticas de grafos;
• Programas orientado a objetos de modelação formal,
• Rede de Petri.

Dentre muitos outros. Vários destes foram mencionados no SBMF(Brasilian Simposium on Formal Methods), um evento bem repercutido dentro e fora do Brasil. Promovido anualmente pela SBC, e que teve esta edição realizada em Natal-Rio Grande do Norte com a organização da Universidade Federal do Rio Grande do Norte(UFRN) e Universidade Federal do Rio Grande do Sul(UFRGS), o evento tem uma característica devota para o campo de teorias e aplicações de Métodos Formais dentro do desenvolvimento de software. A próxima edição já esta sendo preparada, e terá realização em Ouro Preto, Minas Gerais, Brasil. Pode-se esperar que seja tão interessante e produtiva com esta que foi maravilhosamente organizada em Natal-RN, Brasil.

[editar] Vale a pena utilizar métodos formais? E se não utilizarmos? O que poderia acontecer?

Eis alguns exemplos onde o destino dos eventos poderia ser diferente:

• Em julho de 1996 o foguete Ariane 5 (projeto europeu), que carregava satélites científicos explodiu poucos segundos após seu lançamento. Aos 37 segundos de vôo, o software do sistema de navegação (SRI), que foi reutilizado do Ariane 4, emitiu sinais incorretos aos motores, estes giraram sobre um eixo de tal maneira que os controladores de terra iniciaram a autodestruição e o foguete e a sua carga foram destruídos. Continha quatro satélites que custavam ao todos U$ 500 milhões. A falha do software ocorreu em uma tentativa de converter um número 64-bits de ponto flutuante para um inteiro 16-bits, fazendo com que ocorresse um erro numérico muito conhecido na computação, o (overflow), logo a anomalia ocorrida não foi devida a um erro aleatório e sim a um erro de projeto.
• Sistema de triagem/controle de bagagem do aeroporto internacional de Denver (EUA). O sistema atrasou a inauguração do aeroporto. O custo do sistema foi de U$193 milhões. A inauguração estava prevista para out/1993. Em junho de 1994 o sistema ainda não estava funcionando. No começo de 1995 um controle MANUAL de bagagem foi instalado para que o aeroporto pudesse ser inaugurado (com atraso de mais de um ano).
• O Therac-25, um equipamento de radioterapia controlado por computador, aplicou doses fatais de radiação em alguns pacientes de câncer.
• Quando decidiram testar o subsistema de desligamento de emergência da Sizewell-B, uma usina nuclear na Inglaterra, obtiveram falha em mais de 50% das vezes. Não conseguiram encontrar a razão da falha nas 100.000 linhas de código.

Com estes exemplos, entre outros, devemos pensar o quão indispensável é o uso de métodos formais em sistemas de alta integridade. Se nestes projetos tivessem sido usados métodos formais, o custo seria ainda maior, porém, até que ponto a economia fala mais alto do que prejuízos e/ou vidas?

[editar] Veja também e aumente a Wikipedia!

Aqui, estão separados alguns links sobre este tema que não estão disponíveis na Wikipedia em português. Há uma variedade de métodos formais e notações disponíveis, incluindo:

• Máquinas de Estado Abstratas;
• Linguagem Alloy;
• Método B;
• Processo Calculi;
• Processo de comunicação sequencial;
• π-calculus;
• Modelo Formal de Ator;
• Linguagem Esterel;
• Linguagem de programação Lustre;
• Linguagem de especificação RAISE;
• Método de desenvolvimento Viena (VDM),
• Notação Z.
• Especificação formal
• Provadores de teoremas;
• Provador de teorema automatico;
• Verificador de modelos;
• Maquinas oracúlos;
• Modelos de Verificação;
• Pessoas ligadas a Métodos Formais,
• Linguagem de Modelação Rebeca.

[editar] Veja também, em português

• Rede de Petri
• Engenharia de Software
• Desastres de engenharia de Software

[editar] Conclusão

Métodos formais são complementares aos métodos tradicionais, na maioria dos casos reduzem, mas não exterminam os erros. O uso de métodos formais pode ocorrer de forma parcial, ou seja, métodos formais leves, que gerarão uma relação custo-benefício melhor de forma completa e custosa. Os mesmos métodos possibilitam várias análises sobre o comportamento e funcionamento do sistema durante sua especificação e desenvolvimento. A solução de problemas e o desenvolvimento de algoritmos representam uma área muito importante para o desenvolvimento de software, para medir a qualidade dos produtos e indicar possíveis otimizações. A investigação de soluções exatas, como a formalização e comparação de métodos de desenvolvimento de algoritmos e análise da complexidade dos algoritmos gerados, tanto para ambientes seqüenciais quanto paralelos, têm sido bastante pesquisadas. Esperamos que os representantes desta inovadora área consigam sistemas mais ousados, eficazes, onde os métodos formais possam ser aplicados de forma precisa, resultando na solução de vários mistérios da computação.

[editar] Referências

Esta apresentação também está em inglês. Visite Formal Methods.

[editar] Ligações externas

• Sociedade Brasileira de Computação (Página de Métodos Formais);
• Puc-RS;
• Foldoc:Formal Methods;
• Publicações de métodos formais;
• Livraria virtual de métodos formais;
• Quem está nos métodos formais
• Encontros;
• Organizações,
• Companhias.