O que são Métodos Formais
É muito difícil garantir a qualidade de software a partir de inspeções informais, tanto pelo tamanho do software como pela complexidade das linguagens e paradigmas de programação. Métodos Formais são “técnicas baseadas na matemática para descrever propriedades de um sistema”. São usados para a especificação, construção por refinamento e verificação de sistemas de software e hardware, com o objetivo de atingir níveis de qualidade mais elevados e aumentar a confiança na correção do software através de provas formais, refinamentos e testes.
Os componentes de um método formal são: a linguagem de especificação e modelagem formal e o sistema de raciocínio formal (para verificação e análise formal). Métodos de Especificação Formal possuem sintaxe e semântica formais para a especificação dos dados, comportamento e funções de um sistema. Quando métodos formais são usados no desenvolvimento de um sistema, eles servem de base para a sua verificação formal e permitem a descrição de sistemas complexos a partir de entidades abstratas independentes de implementação.
Especificação Formal
A expressão “especificação formal” pode ser entendida de diferentes formas. No sentido comum, uma especificação é formal se for escrita, comunicável, matemática, precisa, não ambígua e sirva de suporte à análise e permita raciocínio e predição. Os matemáticos reforçam que uma especificação só será formal se suportar raciocínio e predição perante o grupo ligado às Métodos Formais em Engenharia de Software. Os engenheiros de software situam-se num campo intermédio concordando que a especificação tem que ser precisa, não ambígua e deve suportar análise.
Vantagens da Especificação Formal
Dentre as principais vantagens do uso de especificação formal estão: a melhor compreensão dos requisitos e o desenho do sistema. Com uma especificação formal e uma linguagem de programação formal é possível provar que o programa está de acordo com a especificação.
As especificações formais podem ser processadas automaticamente (uma vez que a sintaxe e semântica são formais) permitindo o desenvolvimento de ferramentas de especificação. Dependendo da linguagem de especificação usada é possível animar a especificação formal produzindo um protótipo do sistema. Uma especificação formal é constituída por entidades matemáticas e por isso permite manipulação matemática
Aplicações
Existem vários usos e aplicações de métodos formais em diferentes áreas da computação, desde a acadêmica até a industrial. Nos tópicos abaixo estão descritos alguns exemplos de utilização.
Desenvolvimento de Sistemas Multimídia
Cláudia Araújo Ribeiro (UFPE) utiliza em seu trabalho na especificação formal do estado, do comportamento funcional das relações temporais e dos requisitos não-funcionais (novo), com as ferramentas Object-Z e RT-LOTOS.
Modelagem de Sistemas Computacionais usando Redes de Petri
As redes de Petri facilitam a modelagem de características típicas dos problemas de computação como concorrência, controle, conflitos, sincronização, compartilhamento, entre outros. Exemplos de modelagem de sistemas computacionais usando Redes de Petri Ordinárias, Coloridas e Estocásticas: Semáforo, A relação Produtor/Consumidor, Em um sistema PRAM, protocolos de comunicação, paralelismo pipelined, modela um sistema de filas do tipo FIFO (First In-First Out). No trabalho de Leandro Dias da Silva (UFPB) é apresentada uma solução de desenvolvimento sistemático de modelos de sistemas flexíveis de manufatura suportando reuso de modelos de redes de Petri.
Manutenção e Usabilidade de Sistemas Interativos
Um trabalho que se propõe efetuar consiste em unir uma abordagem para a aplicação de métodos formais no contexto da engenharia reversa de sistemas interativos, sendo explorada a possibilidade da adoção destes métodos de forma a validar posteriormente a usabilidade do sistema.
Uso industrial de Métodos Formais
Vários projetos de grande escala tem utilizado a prática de CP-nets e suas ferramentas, sendo muitos desses projetos realizados em um ambiente industrial. Alguns desses exemplos são: em protocolos e redes (TCP, IEEE 802.6, modelagem e análise WAP, IOTP), em softwares (interação em telefones móveis Nokia, execução de programação distribuída), processos empresariais (UML), hardware (chip VSLI), controles de sistemas (controle aéreo da Alemanha), sistemas militares e outros.
Posts relacionados:
- Métodos de Gauss-Seidel e Gauss-Jacobi
- Características Essenciais no Projeto de Linguagens de Programação
- Latinoware 2007
- Vantagens e os desafios de sistemas de comunicações via satélite Low Earth Orbit (LEO)
- Maratonas de Programação 2007
Tags: metodos formais