Верификация интеграции данных в интегрированной системе баз данных по свойствам неорганических веществ и материалов
https://doi.org/10.26907/2541-7746.2025.2.367-383
Аннотация
С ростом неоднородности моделей и схем данных в современном мире все более необходимой становится интеграция данных. Системы интеграции данных создаются в различных предметных областях, например, в астрономии, управлении землепользованием и материаловедении. Программы интеграции данных могут быть очень сложными, а потому становятся важными вопросы формальной верификации их корректности.
В настоящей работе рассмотрен подход к верификации корректности интеграции данных в интегрированной системе баз данных по свойствам неорганических веществ и материалов Института металлургии и материаловедения им. А.А. Байкова РАН. Интеграция данных в этой системе проводится в два этапа: на первом этапе данные из источников, помеченные на удаление, изменение или добавление, преобразуются в промежуточное XML-представление; на втором этапе для элементов XML-представления вызываются процедуры целевой интегрированной базы данных, удаляющие, изменяющие или добавляющие в нее соответствующие записи. Реализация программ интеграции данных осуществлена с использованием композиции императивного языка программирования и декларативного языка реляционных баз данных. Подход к верификации основан на определении семантики схем данных и программ интеграции данных в формальном языке спецификаций и последующем доказательстве корректности интеграции данных с использованием автоматизированных средств доказательства.
При поддержке: Работа выполнена в рамках темы государственного задания ФИЦ ИУ РАН. Автор благодарит Виктора Дударева (Ruhr University Bochum, ИМЕТ РАН) за ценные замечания к работе.
Об авторе
С. А. Ступников
Федеральный исследовательский центр «Информатика и управление» Российской академии наук
Россия
Россия
Сергей Александрович Ступников, ведущий научный сотрудник
г. Москва
Список литературы
1. Masmoudi M., Ben Abdallah Ben Lamine S., Karray M.H., Archimede B., Zghal H.B. Semantic data integration and querying: A survey and challenges // ACM Comput. Surv. 2024. V. 56, No 8. Art. 209. https://doi.org/10.1145/3653317.
2. The Binary Star Database. ИНИСАН, 2025. https://bdb.inasan.ru/.
3. Крупный научный проект фундаментальных исследований «Актуальные научные задачи стратегии адаптации потенциала землепользования России в современных условиях беспрецедентных вызовов (экономический кризис, изменения климата, кризис глобальных тенденций природопользования)». Почвенный институт им. В.В. Докучаева, 2023. https://www.esoil.ru/activities/projects_programs/minobr/knp_2020/.
4. Интегрированная система баз данных по свойствам неорганических веществ и материалов. ИМЕТ РАН, 2025. https://imet-db.ru/.
5. White N., Matthews S., Chapman R. Formal verification: Will the seedling ever flower? // Phil. Trans. R. Soc. A. 2017. V. 375, No 2104. Art. 20150402. https://doi.org/10.1098/rsta.2015.0402.
6. Guagliardo P., Libkin L. A formal semantics of SQL queries, its validation, and applications // Proc. VLDB Endowment (PVLDB). 2017. V. 11, No 1. P. 27–39. https://doi.org/10.14778/3151113.3151116.
7. Rahim L.Ab., Whittle J. A survey of approaches for verifying model transformations // Software Syst. Model. 2015. V. 14, No 2. P. 1003–1028. https://doi.org/10.1007/s10270-013-0358-0.
8. Abrial J.-R. The B-Book: Assigning Programs to Meanings. New York, NY: Cambridge Univ. Press, 1996. xxxiv, 779 p. https://doi.org/10.1017/CBO9780511624162.
9. Atelier B: The industrial tool to efficiently deploy the B Method. 2025. http://www.atelierb.eu/.
10. Butler M., K¨orner P., Krings S., Lecomte T., Leuschel M., Mejia L.-F., Voisin L. The first twenty-five years of industrial use of the B-Method // ter Beek M.H., Ni˘ckovi´c D. (Eds.) Formal Methods for Industrial Critical Systems (FMICS 2020). Ser.: Lecture Notes in Computer Science. V. 12327. Cham: Springer, 2020. P. 189–209. https://doi.org/10.1007/978-3-030-58298-2_8.
11. Stupnikov S. Semantics and verification of entity resolution and data fusion operations via transformation into a formal notation // Kalinichenko L., Kuznetsov S., Manolopoulos Y. (Eds.) Data Analytics and Management in Data Intensive Domains (DAMDID/RCDL 2016). Ser.: Communications in Computer and Information Science. V. 706. Cham: Springer, 2017. P. 145–162. https://doi.org/10.1007/978-3-319-57135-5_11.
12. Stupnikov S.A. Query-driven verification of data integration in the RDF data model // Lobachevskii. J. Math. 2023. V. 44, No 1. P. 205–218. https://doi.org/10.1134/S1995080223010389.
13. Kiselyova N.N., Dudarev V.A., Zemskov V.S. Computer information resources of inorganic chemistry and materials science // Russ. Chem. Rev. 2010. V. 79, No 2. P. 145–166. https://doi.org/10.1070/RC2010v079n02ABEH004104.
14. Kiselyova N.N., Dudarev V.A., Stolyarenko A.V. Integrated system of databases on the properties of inorganic substances and materials // High Temp. 2016. V. 54, No 2. P. 215–222. https://doi.org/10.1134/S0018151X16020085.
15. Kiselyova N.N., Dudarev V.A., Korzhuyev M.A. Database on the bandgap of inorganic substances and materials // Inorg. Mater.: Appl. Res. 2016. V. 7, No 1. P. 34–39. https://doi.org/10.1134/S2075113316010093.
16. Steinberg D., Budinsky F., Paternostro M., Merks E. EMF: Eclipse Modeling Framework. The Eclipse Ser. Addison-Wesley, 2008. 744 p.
17. ATL – a model transformation technology. 2025. https://eclipse.org/atl/.
Рецензия
Для цитирования:
Ступников С.А. Верификация интеграции данных в интегрированной системе баз данных по свойствам неорганических веществ и материалов. Ученые записки Казанского университета. Серия Физико-математические науки. 2025;167(2):367-383. https://doi.org/10.26907/2541-7746.2025.2.367-383
For citation:
Stupnikov S.A. Verification of data integration in an integrated system of databases on the properties of inorganic substances and materials. Uchenye Zapiski Kazanskogo Universiteta. Seriya Fiziko-Matematicheskie Nauki. 2025;167(2):367-383. (In Russ.) https://doi.org/10.26907/2541-7746.2025.2.367-383
Просмотров:
19
Послать статью по эл. почте 