Modelo de métodos formais

O modelo de métodos formais engloba um conjunto de atividades que conduzem à especificação

matemática formal do soTftware. Os métodos formais possibilitam especificar, desenvolver

e verificar um sistema baseado em computador através da aplicação de uma notação matemática

rigorosa. Uma variação dessa abordagem, chamada engenharia de software "cleanroom" (sala

limpa/leve/nítida) [Mil87, Dye92], é aplicada atualmente por algumas organizações de desenvolvimento

de software.

Quando são utilizados métodos formais durante o desenvolvimento, estes oferecem

um mecanismo que elimina muitos dos problemas difíceis de ser superados com o uso.

de outros paradigmas de engenharia de software. Ambiguidade, incompletude e inconsistência

podem ser descobertas e corrigidas mais facilmente - não por meio de uma revisão local, mas

devido à aplicação de análise matemática. Quando são utilizados métodos formais durante o

projeto, servem como base para verificar a programação e, portanto, possibilitam que se descubra

e se corrijam erros que, de outra forma, poderiam passar despercebidos.

Embora não seja uma abordagem predominante, o modelo de métodos formais oferece a

promessa de software sem defeitos. No entanto, foram mencionados motivos para preocupação

a respeito de sua aplicabilidade em um ambiente de negócios:

• Atualmente, o desenvolvimento de modelos formais consome muito tempo e dinheiro.

• Pelo fato de poucos desenvolvedores de software possuírem formação e experiência necessárias

(background) para aplicação dos métodos formais, é necessário treinamento

extensivo.

• É difícil usar os modelos como um meio de comunicação com clientes tecnicamente despreparados

(não sofisticados tecnicamente).

Apesar de tais preocupações, a abordagem de métodos formais tem conquistado adeptos

entre os desenvolvedores de software que precisam desenvolver software com fator crítico de

segurança (como, por exemplo, os desenvolvedores de sistemas aviônicos para aeronaves e

equipamentos médicos), bem como entre desenvolvedores que sofreriam pesadas sanções econômicas

se ocorressem erros no software.