| |
| Acadêmico(a): Fernanda Gums |
| Título: Verificador de Propriedades em Gramática de Grafos |
| |
| Introdução: |
| O desenvolvimento de sistemas, concorrentes ou não, tem sido uma tarefa árdua, tornando necessária a especificação de forma completa e livre de erros. Visando auxiliar este processo, existem métodos formais que são utilizados para construir modelos que descrevem o comportamento do sistema. Segundo Ribeiro (2000, p. 3), a especificação deve ser compacta, precisa e sem ambigüidade, ou seja, feita em uma linguagem com sintaxe e semântica precisamente definidas, utilizando conceitos matemáticos. Estes conceitos são importantes para especificar sistemas, pois permitem afirmar se “um sistema computacional apresenta uma certa propriedade ou satisfaz sua especificação” (DÉHARBE et al., 2000, p. 31). A especificação pode ser total ou parcial: é total quando descreve todo o comportamento desejado do sistema e é parcial quando descreve algumas propriedades que são necessárias para que o sistema possa operar. A especificação parcial é também conhecida como verificação de propriedades. Como exemplo de método formal pode-se citar as gramáticas de grafos, que vêm sendo estudadas desde os anos 70 e têm sido aplicadas em campos da Ciência da Computação que requerem modelos de grafos dinâmicos (grafos que podem sofrer transformações ou manipulações em sua estrutura). Este formalismo consiste em um grafo inicial, que simboliza quais vértices e arestas estão presentes quando ele é iniciado, e um conjunto de regras, que representam os possíveis mapeamentos (morfismos) que podem modificar o estado do sistema. As gramáticas de grafos permitem a especificação de linguagens formais, reconhecimento de padrões, construção de compiladores, modelagem de sistemas concorrentes e distribuídos, projetos de banco de dados e modelagem de sistemas biológicos (RUSSO, 2003, p. 11). Diante do exposto, propõe-se o desenvolvimento de uma ferramenta para especificação formal de sistemas utilizando gramáticas de grafos, onde será possível modelar de forma visual, o grafo inicial e o conjunto de regras que definem a gramática. Para que a modelagem seja feita de forma intuitiva, faz-se necessária a utilização da biblioteca gráfica Java Graph (JGraph). Após a definição da gramática, será possível verificar: a alcançabilidade, que indica quais vértices são alcançáveis ou não; a aplicabilidade, que identifica quais regras são aplicadas no sistema e quais nunca serão aplicadas; e o conflito, que encontra situações em que, concorrentemente, duas regras tentam modificar um objeto ao mesmo tempo. |
| |
|
