Publicado em: 01/06/2010
Tese de Doutorado em Métodos Formais
UNIVERSIDADE FEDERAL DO RIO GRANDE DO SUL
INSTITUTO DE INFORMÁTICA
PROGRAMA DE POS-GRADUAÇÃO EM COMPUTAÇÃO
———————————————————
DEFESA DE TESE DE DOUTORADO
Aluna: Simone André da Costa Cavalheiro
Orientadora: Profa. Dra. Leila Ribeiro
Titulo: Abordagem Relacional de Gramática de Grafos
Linha de Pesquisa: Métodos Formais
Data: 07/06/2010
Hora: 14h
Local: Auditório Prof. José Volkmer de Castilho (Verde), Prédio 43424
Banca Examinadora:
Profa. Dra. Anamaria Martins Moreira (UFRN)
Prof. Dr. Alfio Ricardo de Brito Martini (PUCRS)
Prof. Dr. Daltro José Nunes (UFRGS)
Presidente da Banca: Profa. Dra. Leila Ribeiro
Resumo:
Gramática de grafos é uma linguagem formal bastante adequada para sistemas cujos estados possuem uma topologia complexa (que envolvem vários tipos de elementos e diferentes tipos de relações entre eles) e cujo comportamento é essencialmente orientado pelos dados, isto é, eventos são disparados por configurações particulares do estado. Vários sistemas reativos são exemplos desta classe de aplicações, como protocolos para sistemas distribuídos e móveis, simulação de sistemas biológicos, entre outros. A verificação de gramática de grafos através da técnica de verificação de modelos já é utilizada por diversas abordagens. Embora esta técnica constitua um método de análise bastante importante, ela tem como desvantagem a necessidade de construir o espaço de estados completo do sistema, o que pode levar ao problema da explosão de estados. Bastante progresso tem sido feito para lidar com esta dificuldade, e diversas técnicas têm aumentado o tamanho dos sistemas que podem ser verificados. Outras abordagens propõem aproximar o espaço de estados, mas neste caso não é possível a verificação de propriedades arbitrárias. Além da verificação de modelos, a prova de teoremas constitui outra técnica consolidada para verificação formal. Nesta técnica tanto o sistema quanto suas propriedades são expressas em alguma lógica matemática. O processo de prova consiste em encontrar uma prova a partir dos axiomas e lemas intermediários do sistema. Cada técnica tem argumentos pró e contra o seu uso, mas é possível dizer que a verificação de modelos e a prova de teoremas são complementares. A maioria das abordagens utilizam verificadores de modelos para analisar propriedades de computações, isto é, sobre a seqüência de passos de um sistema. Propriedades sobre estados alcançáveis só são verificadas de forma restrita. O objetivo deste trabalho é prover uma abordagem para a prova de propriedades de grafos alcançáveis de uma gramática de grafos através da técnica de prova de teoremas. Propõe-se uma tradução (da abordagem Single-Pushout) de gramática de grafos para uma abordagem lógica e relacional, a qual permite a aplicação de indução matemática para análise de sistemas com espaço de estados infinito. Definiu-se gramática de grafos utilizando estruturas relacionais e aplicações de regras com lógica de primeira-ordem. Inicialmente considerou-se o caso de grafos (tipados) simples, e então se estendeu a abordagem para grafos com atributos e gramáticas com condições negativas de aplicação. Além disso, baseado nesta abordagem, foram estabelecidos padrões para a definição, codificação e reuso de especificações de propriedades. O sistema de padrões tem o objetivo de auxiliar e simplificar a tarefa de especificar requisitos de forma precisa. Finalmente, propõe-se implementar definições relacionais de gramática de grafos em estruturas de event-B, de forma que seja possível utilizar os provadores disponíveis para event-B para demonstrar propriedades de gramática de grafos.
Palavras-Chave: Gramática de Grafos, prova de teoremas, lógica de primeira ordem, especificação formal, verificação formal
INSTITUTO DE INFORMÁTICA
PROGRAMA DE POS-GRADUAÇÃO EM COMPUTAÇÃO
———————————————————
DEFESA DE TESE DE DOUTORADO
Aluna: Simone André da Costa Cavalheiro
Orientadora: Profa. Dra. Leila Ribeiro
Titulo: Abordagem Relacional de Gramática de Grafos
Linha de Pesquisa: Métodos Formais
Data: 07/06/2010
Hora: 14h
Local: Auditório Prof. José Volkmer de Castilho (Verde), Prédio 43424
Banca Examinadora:
Profa. Dra. Anamaria Martins Moreira (UFRN)
Prof. Dr. Alfio Ricardo de Brito Martini (PUCRS)
Prof. Dr. Daltro José Nunes (UFRGS)
Presidente da Banca: Profa. Dra. Leila Ribeiro
Resumo:
Gramática de grafos é uma linguagem formal bastante adequada para sistemas cujos estados possuem uma topologia complexa (que envolvem vários tipos de elementos e diferentes tipos de relações entre eles) e cujo comportamento é essencialmente orientado pelos dados, isto é, eventos são disparados por configurações particulares do estado. Vários sistemas reativos são exemplos desta classe de aplicações, como protocolos para sistemas distribuídos e móveis, simulação de sistemas biológicos, entre outros. A verificação de gramática de grafos através da técnica de verificação de modelos já é utilizada por diversas abordagens. Embora esta técnica constitua um método de análise bastante importante, ela tem como desvantagem a necessidade de construir o espaço de estados completo do sistema, o que pode levar ao problema da explosão de estados. Bastante progresso tem sido feito para lidar com esta dificuldade, e diversas técnicas têm aumentado o tamanho dos sistemas que podem ser verificados. Outras abordagens propõem aproximar o espaço de estados, mas neste caso não é possível a verificação de propriedades arbitrárias. Além da verificação de modelos, a prova de teoremas constitui outra técnica consolidada para verificação formal. Nesta técnica tanto o sistema quanto suas propriedades são expressas em alguma lógica matemática. O processo de prova consiste em encontrar uma prova a partir dos axiomas e lemas intermediários do sistema. Cada técnica tem argumentos pró e contra o seu uso, mas é possível dizer que a verificação de modelos e a prova de teoremas são complementares. A maioria das abordagens utilizam verificadores de modelos para analisar propriedades de computações, isto é, sobre a seqüência de passos de um sistema. Propriedades sobre estados alcançáveis só são verificadas de forma restrita. O objetivo deste trabalho é prover uma abordagem para a prova de propriedades de grafos alcançáveis de uma gramática de grafos através da técnica de prova de teoremas. Propõe-se uma tradução (da abordagem Single-Pushout) de gramática de grafos para uma abordagem lógica e relacional, a qual permite a aplicação de indução matemática para análise de sistemas com espaço de estados infinito. Definiu-se gramática de grafos utilizando estruturas relacionais e aplicações de regras com lógica de primeira-ordem. Inicialmente considerou-se o caso de grafos (tipados) simples, e então se estendeu a abordagem para grafos com atributos e gramáticas com condições negativas de aplicação. Além disso, baseado nesta abordagem, foram estabelecidos padrões para a definição, codificação e reuso de especificações de propriedades. O sistema de padrões tem o objetivo de auxiliar e simplificar a tarefa de especificar requisitos de forma precisa. Finalmente, propõe-se implementar definições relacionais de gramática de grafos em estruturas de event-B, de forma que seja possível utilizar os provadores disponíveis para event-B para demonstrar propriedades de gramática de grafos.
Palavras-Chave: Gramática de Grafos, prova de teoremas, lógica de primeira ordem, especificação formal, verificação formal