Formal verification of attributed and typed graph transformation systems

In this paper we present an approach to software analysis using model checking. To do so, the system must be specified through attributed and typed graph transformation. Using attributed graphs helps to model object oriented systems and using typed graphs makes it possible to support metamodeling techniques. To complete the development process with graphs, we propose model checking. As it is not feasible to verify graph systems directly, so we render them into the BIR-the input language of Bogor model checker- and then the verification will be done by Bogor.