Design by contract is a software development methodology that uses contracts for defining interfaces among interacting components of a software system. Graph transformation system is used to specify the behavioral aspects of software components by defining the pre- and post-conditions of methods as contracts. In this paper, we focus on testing executable software models specified by a graph transformation system. A set of model-specific coverage criteria and a cost-aware search-based test generation approach are introduced. To evaluate the effectiveness of the proposed coverage criteria and the test generation approach, a type of mutation analysis is presented at the model level. Furthermore, a couple of fault-detection methods are used to assess the quality of the generated tests in the model-level mutation analysis. The proposed approach is implemented in GROOVE, a toolset for model checking graph transformation systems. The empirical results based on some well-known case studies demonstrate the efficiency and scalability of each proposed coverage criterion and testing approach. The comparison of the proposed test generation approach with state-of-the-art techniques indicates a significant improvement in terms of fault-detection capability and testing costs.
