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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Nonaka, I., Kodama, M., Hirose, A., Kohlbacher, F.: Dynamic fractal organizations for promoting knowledge-based transformation – a new paradigm for organizational theory. Eur. Manag. J. 32(1), 137–146 (2014)
Heavin, C., Power, D.J.: Challenges for digital transformation – towards a conceptual decision support guide for managers. J. Decis. Syst. 27(1), 38–45 (2018)
Mens, T., Czarnecki, K., Gorp, P.V.: A taxonomy of model transformations. Electron. Notes Theor. Comput. Sci. 152, 125–142 (2006)
Degrandsart, S., Demeyer, S., Van den Bergh, J., Mens, T.: A transformation-based approach to context-aware modelling. Softw. Syst. Model. 13(1), 191–208 (2014)
Bergmann, G., Ráth, I., Varró, G., Varró, D.: Change-driven model transformations. Softw. Syst. Model. 11(3), 431–461 (2012)
Schürr, A.: Graph-transformation-driven correct-by-construction development of communication system topology adaptation algorithms. In: Schaefer, I., Karagiannis, D., Vogelsang, A., Méndez, D., Seidl, C. (eds.) Modellierung. LNI, pp. 15–29. Gesellschaft für Informatik, Bonn (2018)
Rahim, L.A., Whittle, J.: A survey of approaches for verifying model transformations. Softw. Syst. Model. 14(2), 1003–1028 (2015)
Akehurst, D., Kent, S.: A relational approach to defining transformations in a metamodel. In: Jézéquel, J.-M., Hussmann, H., Cook, S. (eds.) UML 2002. LNCS, vol. 2460, pp. 243–258. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45800-X_20
Bondavalli, A., Dal Cin, M., Latella, D., Majzik, I., Pataricza, A., Savoia, G.: Dependability analysis in the early phases of UML based system design. Int. J. Comput. Syst. - Sci. Eng. 16(5), 265–275 (2001)
Küster, J.M., Abd-El-Razik, M.: Validation of model transformations – first experiences using a white box approach. In: Kühne, T. (ed.) MODELS 2006. LNCS, vol. 4364, pp. 193–204. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-69489-2_24
Amrani, M., et al.: A tridimensional approach for studying the formal verification of model transformations. In: Verification and Validation of Model Transformations (VOLT) (2012)
Hausmann, J.H., Heckel, R., Sauer, S.: Extended model relations with graphical consistency conditions. In: UML 2002 Workshop on Consistency Problems in UML-Based Software Development, pp. 61–74. Blekinge Institute of Technology (2002)
Ulitin, B., Babkin, E.: Ontology and DSL co-evolution using graph transformations methods. In: Johansson, B., Møller, C., Chaudhuri, A., Sudzina, F. (eds.) BIR 2017. LNBIP, vol. 295, pp. 233–247. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-64930-6_17
Ruffolo, M., Sidhu, I., Guadagno, L.: Semantic enterprise technologies. In: Proceedings of the First International Conference on Industrial Results of Semantic Technologies, vol. 293, pp. 70–84 (2007)
Gogolla, M., Bohling, J., Richters, M.: Validating UML and OCL models in USE by automatic snapshot generation. J. Softw. Syst. Model. 4(4), 386–398 (2005)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Ulitin, B., Babkin, E., Babkina, T., Vizgunov, A. (2019). Automated Formal Verification of Model Transformations Using the Invariants Mechanism. In: Pańkowska, M., Sandkuhl, K. (eds) Perspectives in Business Informatics Research. BIR 2019. Lecture Notes in Business Information Processing, vol 365. Springer, Cham. https://doi.org/10.1007/978-3-030-31143-8_5
Download citation
DOI: https://doi.org/10.1007/978-3-030-31143-8_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-31142-1
Online ISBN: 978-3-030-31143-8
eBook Packages: Computer ScienceComputer Science (R0)