Formal Verification of Object-Oriented Graph Grammars Specifications

Concurrent object-oriented systems are ubiquitous due to the importance of networks and the current demands for modular, reusable, and easy to develop software. However, checking the correctness of such systems is a hard task, mainly due to concurrency and inheritance aspects. In this paper we present an approach to the verification of concurrent object-oriented systems. We use graph grammars equipped with object oriented features (including inheritance and polymorphism) as the specification formalism, and define a translation from such specifications to Promela, the input language of the SPIN model checker.