Finding and Fixing Bugs in Model Transformations with Formal Verification: An Experience Report.
Gehan M. K. Selim, James R. Cordy, Jürgen Dingel, Lucio Levi, Bentley Oakes · PolyPublie (École Polytechnique de Montréal) · 2015
We report on the use of a formal verification tool for a graph-based transformation language in the context of a case study. The tool identified two bugs in the transformation that had eluded all previous testing efforts. The paper describes what we learned about the analysis of model transformations and how we intend to use these insights to improve the verification tool.