The Community for Technology Leaders
Software Testing Verification and Validation Workshop, IEEE International Conference on (2011)
Berlin, Germany
Mar. 21, 2011 to Mar. 25, 2011
ISBN: 978-0-7695-4345-1
pp: 63-66
ABSTRACT
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, we propose a model-driven engineering approach that works the other way around. Instead of making a concrete model more abstract, we propose to refine an abstract model to make it more concrete. We propose to use fine-grained model transformations to enable model checking of models that are as close to the implementation model as possible. We applied our approach in a case study. The results show that models that are more concrete can be validated when fine-grained transformations are applied.
INDEX TERMS
Model-Driven Engineering, Model Transformation, Model Checking, Domain-Specific Language, Verification
CITATION

M. van den Brand, L. Engelen and M. van Amstel, "Using a DSL and Fine-Grained Model Transformations to Explore the Boundaries of Model Verification -- Extended Abstract," Software Testing Verification and Validation Workshop, IEEE International Conference on(ICSTW), Berlin, Germany, 2011, pp. 63-66.
doi:10.1109/ICSTW.2011.8
83 ms
(Ver 3.3 (11022016))