Verifying Object-Based Graph Grammars

• DOI: 10.1016/j.entcs.2004.02.061
• Publication Date: 2004-12-16T20:34:57Z
• Authors: Osmar Marchi dos ...; Fernando Luís Dotti; Leila Ribeiro
• Keywords: visualization of traces; model checking; Graph grammars; Theoretical Computer Science; Computer Science(all)

AbstractObject-Based Graph Grammars (OBGG) is a formal language suitable for the specification of distributed systems. On previous work, a translation from OBGG models to PROMELA (the input language of the SPIN model checker) was defined, enabling the verification of OBGG models using SPIN. This paper builds on these results, where we extend the approach for property specification and define an approach to interpret PROMELA traces as OBGG derivations, generating graphical counter-examples for properties that are not true for an OBGG model.