Model checking is one of the most accurate analysis techniques which are used to verify software and hardware systems. However, the analysis of large and complex systems tends to become infeasible since their state spaces easily become too big. Besides well-known abstraction techniques, which may hamper the accuracy of results, in this paper we propose the use of scenario-driven model checking to address and mitigate the state explosion problem. The proposal starts from systems specified through a Graph Transformation (GT) system and it is focused on the analysis of the most significant scenarios. We exploit the modularity of GT systems to reduce the state space by eliminating all the nodes and rules that are not involved in the scenario. Focused analysis also helps concentrate on the most critical behaviors of the system and smooth the risks associated with them. The paper introduces the analysis approach and explains how scenarios (specified in terms of sequence diagrams) can help to reduce the state space. All main concepts are illustrated through a simple application for a travel agency specified as if it were a service-oriented application.
