Métodos Formais

 

Uma questão fundamental no desenvolvimento de um software é garantir que este é 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. Tendo este modelo formal como base, pode-se:

 
· 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 podendo-se provar que a implementação está correta (geração de código correto).

Entre os vários métodos de especificação formal existentes, destacam-se o método Z, o qual 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. Originalmente, o método Z foi concebido para a especificação de sistemas seqüenciais, mas existem extensões, que permitem a descrição de sistemas concorrentes seguindo o paradigma de cálculo de processos, ou seja, o sistema concorrente é descrito através dos processos que o constituem e das comunicações entre esses processos.

O método de gramática de grafos, que pode ser visto como uma generalização de redes de Petri, já está sendo utilizado por membros da equipe de pesquisa deste projeto como base para a especificação e simulação de sistemas concorrentes, dentro do escopo do projeto PLATUS (projeto integrado - CNPq ). Uma teoria para incluir conceitos de modularização neste formalismo está sendo desenvolvida, baseada na composição de gramáticas e semântica de concorrência. Além disso, no projeto GRAPHIT (cooperação Brasil/Alemanha) estão sendo desenvolvidos conceitos de animação de especificações descritas em gramáticas de grafos, permitindo visualizar a execução/simulação de um sistema de várias formas.

As abordagens utilizando Z combinada a CSP e gramáticas de grafos para especificação são complementares para a descrição de um sistema: a primeira é orientada a processos, enquanto gramáticas de grafos são orientadas a dados.

Neste projeto, além de métodos de especificação formal, métodos para verificação e análise serão considerados.

A verificação de sistemas reativos normalmente emprega alguma forma de lógica temporal, onde se descreve a interação, possivelmente infinita, entre diversos agentes concorrentes de um certo modelo computacional. Estas lógicas permitem expressar de forma conveniente as propriedades esperadas desta interação. Porém, para verificar que um sistema particular apresenta uma propriedade específica, é desejável empregar alguma ferramenta automática, 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. As ferramentas normalmente usadas são provadores de teoremas e verificadores de modelos.

A solução de problemas e desenvolvimento de algoritmos é uma área muito importante para o desenvolvimento de software para medir a qualidade do produto 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. Em particular no PGCC/UFRGS foram desenvolvidas metodologias para cálculo de complexidade no pior caso e caso médio, e para algoritmos recursivos, metodologias para as quais agora, estão sendo desenvolvidas ferramentas computacionais. Além disto, a complexidade de especificações descritas em gramáticas de grafos já está sendo investigada.

[Áreas envolvidas] [topo]