Аннотация:
С ростом неоднородности моделей и схем данных в современном мире все более необходимой становится интеграция данных. Системы интеграции данных создаются в различных предметных областях, например, в астрономии, управлении землепользованием и материаловедении. Программы интеграции данных могут быть очень сложными, а потому становятся важными вопросы формальной верификации их корректности.
В настоящей работе рассмотрен подход к верификации корректности интеграции данных в интегрированной системе баз данных по свойствам неорганических веществ и материалов Института металлургии и материаловедения им. А.А. Байкова РАН. Интеграция данных в этой системе проводится в два этапа: на первом этапе данные из источников, помеченные на удаление, изменение или добавление, преобразуются в промежуточное XML-представление; на втором этапе для элементов XML-представления вызываются процедуры целевой интегрированной базы данных, удаляющие, изменяющие или добавляющие в нее соответствующие записи. Реализация программ интеграции данных осуществлена с использованием композиции императивного языка программирования и декларативного языка реляционных баз данных. Подход к верификации основан на определении семантики схем данных и программ интеграции данных в формальном языке спецификаций и последующем доказательстве корректности интеграции данных с использованием автоматизированных средств доказательства.
Ключевые слова:
интеграция данных, верификация, семантика программ, доказательство корректности.
УДК:
004.62
Поступила в редакцию: 01.03.2025 Принята в печать: 23.03.2025
Полный текст:
PDF файл (484 kB)