On the Features of a Formal Semantics of an Imperative Language for the Data Integration Program Verification

Sergey Stupnikov

Abstract


Increasing number of heterogeneous data sources in science and industry leads to the need for their integration. Specialized data integration systems are being developed in various subject domains. Due to the complexity of data integration programs, formal verification of their correctness becomes an important issue. The correctness of a data integration program is expert-defined property binding the state of a set of data sources and the state of the target integrating database, expressed as a logical formula. The formal verification process can be difficult, but the cost of correcting an error after the system is released into production exceeds the cost of correcting an error at the system development stage by tens or hundreds of times. In practice, data integration programs are often implemented using imperative languages. The paper highlights the features and summarizes the experience in definition the formal semantics of imperative languages for data integration programs verification in the domains of astronomy, materials science, and land use management. The features of defining the semantics of library mathematical and string functions, data transformation functions, assignment statement and auxiliary function invocation, sequential composition of statements, conditional statement, and loop statements are considered. The general principles of application of the formal semantics of imperative programming languages for data integration programs verification using automated proof tools are presented.


Full Text:

PDF (Russian)

References


M. Masmoudi, S. Ben Abdallah Ben Lamine, M. H. Karray, B. Archimede, and H. Baazaoui Zghal, “Semantic data integration and querying: A survey and challenges,” ACM Comput. Surv., vol. 56, no. 8, pp. 1–35, 2024.

D. Kovaleva, P. Kaygorodov, O. Malkov, B. Debray, and E. Oblak, “Binary star DataBase BDB development: Structure, algorithms, and VO standards implementation,” Astron. Comput., vol. 11, pp. 119–125, 2015.

P. Kaygorodov, N. Skvortsov, D. Kovaleva, and O. Malkov, “A new version of the binary star database BDB: Challenges and directions,” Open Astron., vol. 32, no. 1, 2023.

The Binary Star Database. 2025. URL: https://bdb.inasan.ru/

Integrated system of databases on the properties of inorganic substances and materials. Baikov Institute of Metallurgy and Materials Science, Russian Academy of Science. 2025. URL: https://imet-db.ru/

N. N. Kiselyova, V. A. Dudarev, and A. V. Stolyarenko, “Integrated system of databases on the properties of inorganic substances and materials,” High Temp., vol. 54, no. 2, pp. 215–222, 2016.

A major scientific project “Current scientific objectives of the strategy for adapting Russia's land use potential in modern conditions of unprecedented challenges (economic crisis, climate change, crisis of global environmental trends)”. – V.V. Dokuchaev Soil Science Institute, 2023. URL: https://www.esoil.ru/activities/projects_programs/minobr/knp_2020/

V. Nundloll, R. Lamb, B. Hankin, and G. Blair, “A semantic approach to enable data integration for the domain of flood risk management,” Environmental Challenges, vol. 3, no. 100064, p. 100064, 2021.

J.-R. Abrial, The B-book: Assigning programs to meanings. Cambridge, England: Cambridge University Press, 2011.

B Language Reference Manual. Version 1.8.10. ClearSy, 2025.

Atelier B, the industrial tool to efficiently deploy the B Method. 2025. URL: http://www.atelierb.eu/

N. White, S. Matthews, and R. Chapman, “Formal verification: will the seedling ever flower?,” Philos. Trans. A Math. Phys. Eng. Sci., vol. 375, no. 2104, p. 20150402, 2017.

M. Butler et al., “The first twenty-five years of industrial use of the B-method,” in Lecture Notes in Computer Science, Cham: Springer International Publishing, 2020, pp. 189–209.

S. Stupnikov, “Semantics and verification of entity resolution and data fusion operations via transformation into a formal notation,” in Communications in Computer and Information Science, Cham: Springer International Publishing, 2017, pp. 145–162.

S. Stupnikov, “Rule-based specification and implementation of multimodel data integration,” in Communications in Computer and Information Science 822, Cham: Springer International Publishing, 2018, pp. 198–212.

S.A. Stupnikov, “Formal Semantics and Verification of Procedural SQL Programs Implementing Materialized Data Integration,” Lobachevskii J Math, 2025. In print.

S.A. Stupnikov, “Verification of data integration in the integrated system of databases on the properties of inorganic substances and materials,” Uchenye Zapiski Kazanskogo Universiteta. Seriya Fiziko-Matematicheskie Nauki, 167(2), 2025. In print.

P. D. Mosses, “Formal Semantics of Programming Languages: An Overview,” Electronic Notes in Theoretical Computer Science, 148(1), pp. 41-73, 2006.

D. Guth, “A formal semantics of Python 3.3,” Doctoral dissertation, University of Illinois at Urbana-Champaign, 2013.

M. A. Köhl, “An executable structural operational formal semantics for Python,” Master Thesis, Saarland University, 2020. URL: https://embedded.cs.uni-saarland.de/publications/theses/thesis_cs_msc_Koehl_Maximilian.pdf


Refbacks

  • There are currently no refbacks.


Abava  Кибербезопасность ИТ конгресс СНЭ

ISSN: 2307-8162