Modelo de Métodos Formais

Os métodos formais são técnicas baseadas em formalismos matemáticos que podem ser usados para a especificação, desenvolvimento e verificação de sistemas de software. Seu uso para o desenvolvimento de software é motivado pela base que fornecem garantindo confiabilidade e robustez a um projeto, uma vez que executam análises matemáticas apropriadas. No entanto, o alto custo do uso de métodos formais restringe o seu uso ao desenvolvimento de sistemas de alta integridade, no qual há alta probabilidade das falhas conduzirem à perda de vidas ou sérios prejuízos (como nas missões espaciais e no controle de voos, por exemplo). 

Ônibus espacial

Exemplo de sistema crítico. Fonte: Everett Historical/shutterstock

No modelo de Métodos Formais, também conhecido como Engenharia de Software Cleanroom (Sala Limpa), uma questão fundamental é garantir que o software é realmente uma solução para o problema proposto. Para realizar tal tarefa deve-se primeiro construir um modelo da solução (especificação) utilizando uma linguagem formal. (FACIN, 2002). Tendo este modelo formal como base, o método permite:

• realizar provas matemáticas que garantem que este modelo possui as propriedades requisitadas (verificação);
• analisar se a solução proposta é aceitável do ponto de vista de desempenho, indicando quais as melhores estratégias para implementação a serem seguidas;
• validar o modelo através de simulações;
• realizar o desenvolvimento do software, sendo possível provar que a implementação está correta (geração de código correto).

Dentre os vários métodos de especificação formal existentes, destacam-se o método Z, que já foi utilizado em várias aplicações práticas, e o método de gramáticas de grafos, por possuir uma linguagem visual de representação e descrever com naturalidade fenômenos de sistemas concorrentes.

De uma maneira mais abrangente, podemos caracterizar assim o modelo de Métodos Formais:

• Permite especificar, desenvolver e verificar um software através de uma rigorosa notação matemática;
• Fornece um mecanismo para eliminar muitos problemas encontrados nos outros modelos, como ambiguidade, incompletude e inconsistência, que podem ser descobertos e corrigidos mais facilmente através de análise matemática;
• Promete o desenvolvimento de software livre de defeitos;
• Consome muito tempo de desenvolvimento e é muito caro.

Como poucos desenvolvedores possuem o conhecimento necessário para utilizá-lo, são requeridos muitos cursos e treinamentos. É difícil usar tais modelos matemáticos formais como meio de comunicação com a maioria dos clientes. Assim, como já dissemos, sua área de aplicação é muito restrita, abrangendo, principalmente, aplicações críticas.