Specification of Models Based on Contexts using Graph Grammars

This paper presents an approach for model specification in the context of Model Checking, using graph grammars. The choice for this formal method is justified by the visual language provided by Graph Grammar and the possibility of using it to check properties of a system. Our approach is based on the analysis of a graph grammar obtained from trace information generated by Java applications. The process of creating such graph grammar from execution traces follows the main ideas of an existing approach that allows the generation of labeled transition systems from Java code. The main objective of this work is to find a way to automate the process of generating a graph grammar, using the information extracted from the source code and execution traces. For this, we developed an algorithm that maps system information, such as values of variables and possible transitions between states of a program, to rules of a graph grammar. To evaluate the methodology used in our approach, we conducted two experiments with toy applications and discuss the results obtained.