Automated Formal Verification of Model Transformations Using the Invariants Mechanism

Abstract

The article is devoted to the problem of automated formal verification of modeling artifacts during engineering of digital transformations. Automation significantly increases the quality of model transformations since many manual errors are eliminated. However, the formal checking the correctness of such automation remains an open question. One more problem is the dependence of the procedure for checking the correctness of transformations on the modeling languages of the source and target models. In the article we represent the solution, based on the formalism of invariant checking, that allows modelers to formally test the correctness of model transformation regardless of a modeling language.