Using a DSL and Fine-Grained Model Transformations to Explore the Boundaries of Model VerifiCation
Traditionally, the state-space explosion problem in model checking is handled by applying abstractions and simplifications to the model that needs to be verified. In this paper, the authors propose a model-driven engineering approach that works the other way around. Instead of making a concrete model more abstract, they propose to refine an abstract model to make it more concrete. They propose to use fine-grained model transformations to enable model checking of models that are as close to the implementation model as possible. They applied the approach in a case study. The results show that it is possible to validate models that are more concrete when fine-grained transformations are applied.