Banca de TCC: Alex Bertei

UNIVERSIDADE FEDERAL DE PELOTAS
CENTRO DE DESENVOLVIMENTO TECNOLÓGICO
TRABALHO DE CONCLUSÃO DE CURSO

Apresentações Finais (2014/1)

Uma tradução de Gramática de Grafos Controlada para Event-B
por
Alex Bertei

Curso:
Ciência da Computação

Banca:
Profa. Luciana Foss (orientador)
Profa. Simone André da Costa Cavalheiro (co-orientador)
Profa. Renata Hax Sander Reiser
Prof. André Rauber Du Bois
Profa. Aline Brum Loreto

Data: 17 de Julho de 2014

Hora: 08:30h

Local: Sala 414

Resumo do Trabalho:

A cada dia que passa sistemas ficam mais complexos e sofisticados. Com isso, a tarefa de especificar um sistema não é fácil e nem natural. Para garantir certas propriedades de um sistema, este deve ser especificado através de uma linguagem que ofereça métodos de análise. Diversas técnicas e metodologias são utilizadas para fazer essas especificações. O fato das técnicas difundidas no mercado permitirem gerar resultados diferentes do que foi especificado fez com que surgisse a necessidade de utilizar métodos formais para especificações e verificações de sistemas. Neste caso o sistema é especificado formalmente através de um modelo matemático. Gramática de Grafos (GG) é uma linguagem formal bastante adequada para especificar sistemas complexos. Em uma GG os estados do sistema são representados por grafos e as mudanças entre os estados como regras. O uso de GGs é interessante pelo fato de existirem diferentes técnicas para a especificação e verificação de sistemas que são descritos nesta linguagem. Além disso, as GGs possuem um layout gráfico, que é bastante intuitivo, o que torna a linguagem de fácil entendimento até para os não teóricos. Gramáticas de grafos controladas (GGC) são GGs que permitem definir uma ordem na aplicação das regras, onde não é levado em conta o estado, e sim uma estrutura de controle auxiliar. Entretanto, para esse tipo de gramática não existem ferramentas que permitem a verificação formal de propriedades. Assim a proposta deste trabalho é estender a abordagem de gramática de grafos que permite o uso de provadores de teoremas para análise de propriedades, para suportar estruturas de controle para a aplicação das regras. Com isso, a principal contribuição deste trabalho, será possibilitar o uso de provadores de teoremas para fazer a verificação de propriedades de Sistema Multiagentes (SMAs). Pois existe uma abordagem que usa GGC para especificar SMAs.

Para mais informações acesse: http://inf.ufpel.edu.br/nopcc/doku.php?id=bancas:2014_1