Occurrence graph grammars with negative application conditions

Abstract

Graph Grammars are based on the application of rules that are able to modify graphs, as such, they provide a suitable formalism to model complex systems in an intuitive and precise manner, providing both a graphical language and a solid formal background for systems analysis. Therefore, they have been used in a wide range of applications within Computer Science, specially in the field of Model-Driven Development. Particularly, the study of the Semantics of Graph Grammars, i.e. which graphs belong to the language of a grammar and which derivations are possible within the context of a grammar, provides a powerful framework for reasoning about the execution behaviour of systems modelled as Graph Grammars. There are several different ways of specifying the Semantics of Graph Grammars. One notable possibility is the use of Occurrence Graph Grammars, which encodes the Semantics in a structure that is also a Graph Grammar itself. Occurrence Graph Grammars differ from other semantic models such as Unfolding and Canonical Derivations mainly by providing a more compact, easier to analyse structure. They were introduced in the nineties and used ever since, however the original definitions lack the inclusion of Negative Application Conditions, additional structures imposed over the rules of a grammar to better tune their possible applications according to the execution context. Given the important role Negative Application Conditions play in the modelling and analysis of complex systems as Graph Grammars nowadays, this thesis presents an extension of the framework of Occurrence Graph Grammars to include them. It also presents its implementation in Verigraph, a system specification and verification tool based on graph rewriting.

Gramáticas de Grafos baseiam-se na aplicação de regras que modificam grafos, fornecendo assim um formalismo adequado para a modelagem de sistemas complexos de forma intuitiva e precisa, além de fornecer uma notação gráfica descomplicada e uma base formal sólida para a análise de sistemas. Dados tais atributos, essas gramáticas possuem uma ampla gama de aplicações dentro da Ciência da Computação, especialmente no campo do Desenvolvimento Orientado a Modelos. Particularmente, o estudo da semântica de Gramáticas de Grafos (isto é, quais grafos pertencem à linguagem da gramática e quais derivações são permitidas no contexto da gramática) provê uma poderosa ferramenta para compreender e analisar o comportamento de sistemas modelados como Gramáticas de Grafos. Existem diversas formas de especificar a semântica de Gramáticas de Grafos, uma delas é o uso de Gramáticas de Grafos de Ocorrência que codificam tal semântica em estruturas que também são, por sua vez, Gramáticas de Grafos. O uso de Gramáticas de Grafos de Ocorrência ao invés de outros modelos semânticos, como por exemploUnfolding e Derivações Canônicas, possui a vantagemde fornecer uma estrutura mais compacta e fácil de analisar. Gramáticas de Ocorrência foram introduzidas nos anos noventa e utilizadas desde então, porém as definições originais não incluem o uso de Condições Negativas de Aplicação, estruturas adicionais anexadas às regras de uma gramática para refinar as possíveis aplicações das regras em determinados contextos. Dada a atual importância das Condições Negativas de Aplicação na modelagem de sistemas complexos, essa dissertação propõe uma extensão da teoria das Gramáticas de Grafos de Ocorrência de forma a incluílas, além de apresentar a implementação desta teoria no Verigraph, uma ferramenta de especificação e verificação de sistemas baseada em reescrita de grafos.