VeriGraph : a tool for model checking graph grammars

Abstract

In this work, we present the construction of a tool for model checking graph grammars, VeriGraph. The verification is done by first executing a specification written as a graph grammar, resulting in a state space, and then checking properties of this specification with a CTL model checker. These functions are built with low coupling, and can be used in conjunction, as we do here, or reused for other implementations as needed. The tool focuses on flexibility, so it can be used to test new ideas about system simulation and verification techniques using graph grammars. The graph grammar approach we use is the double pushout approach. We present a brief review of the theory, including the its main structures and algorithms for rewriting. Using double pushout as our approach poses some restrictions on the rewriting, which we take advantage to write a simple algorithm that is O(V E) on the number of nodes N and edges E of the left hand side of a rule. We then use this structure to build a state space of the executed grammar. The model checker uses a state-transition system based on the graph grammar state space to check for properties expressed in computational tree logic (CTL). We review CTL’s semantics and present an algorithm to perform the satisfaction verification of a CTL formula. The state-transition system is built by using the names of the production that can be applied to a state as the atomic propositions of that state. We discuss the limitations of this method and propose possible solutions to it. The system is developed in Haskell. We review the relevant features of the language that we used when building this application. The algorithm and structure representation used in graph grammar and model checking are presented with code listings. We then present the integration and one experiment to give a notion of how the developed system performs. We plan to continue the development of this tool, and we present what we plan to work on next, such as the implementation of second order graph grammar execution, critical pair analysis, and linear time logic implementation, and general improvements.

Neste trabalho é apresentada a construção de uma ferramenta para a verificação de modelos de gramáticas de grafos, VeriGraph. A verificação é feita a partir da execução de uma gramática de grafos, que resulta em um espaço de estados que é usado para verificar propriedades especificadas em CTL. A funcionalidades do sistema são construídas com baixa acoplamento, e podem ser usadas em conjunto, como aqui fazemos, ou isoladamente em outras implementações. A ferramenta é construída com foco em flexibilidade, para que possa ser usada para testar novas idéias sobre simulação verificação de sistemas usando gramáticas de grafos. Nós usamos o método de reescrita de grafos baseado em double pushout, do qual apresentamos uma breve revisão da teoria, e algoritmos e estruturas usadas na reescrita. O uso de double pushout implica em limitações no processo de reescrita, e nós usamos estas limitações para construir um algoritmo de complexidade O(V E) do número de nodos N e arestas E no lado esquerdo da produção. Nós usamos estas estruturas para construir o espaço de estados da execução. O verificador de modelos usa um sistema de transição de estados basedo no espaço de estados da gramática de grafos para executar a verificação de propriedades expressas como fórmulas em lógica de árvores computacionais (CTL). Nós revisamos a semântica do CTL, e apresentamos um algoritmo para executar a verificação de satisfação de uma fórmula. A construção do sistema de transição de estados é feita usando os nomes das regras que podem ser aplicadas a um dado estado como proposições atômicas deste estado. Este modelo tem limitações, que são discutidas junto com possíveis melhorias. O sistema foi desenvolvido em Haskell. Nós revisamos as principais funcionalidades da linguagem que usamos na implementação. Os algoritmos e estruturas usados na implementação são apresentados junto com as listagens de código relevantes. Por fim, apresentamos a integração de ambos os módulos, e um experimento para dar a noção da performance do sistema. É planejado continuar o desenvolvimento desta ferramenta, e nós apresentamos quais as funcionalidades que pretendemos desenvolver no futuro, como execução de gramáticas de grafos de segunda ordem, análise de par crítico, e implementação de novas formas de model checking, além de melhorias gerais.