Ученые МГУ представили новый метод для автоматизированной верификации корректности интеграции данных в модели данных семантического Веба Resource Description Framework (RDF). Об этом CNews сообщили представители МГУ.
Современные исследовательские инфраструктуры, такие как EUDAT и NDS, накапливают и управляют огромными объемами разнородных научных данных. Чтобы упростить доступ и использование этих данных, исследователи прибегают к интеграции данных, используя единую унифицированную модель для представления данных из различных источников. RDF — это широко используемая эталонная модель данных для интеграции данных в научных инфраструктурах.
Интеграция данных может быть сложным и трудоемким процессом из-за неоднородности схем данных, их форматов и семантики. Поэтому крайне важно проверять корректность интеграции данных.
Предложенный метод верификации обеспечивает автоматизированную формальную проверку корректности интеграции данных. Он основан на отображении схем данных, запросов и представлений в формальный язык Abstract Machine Notation (AMN). AMN — это язык, основанный на логике первого порядка и теории множеств, который позволяет исследователям формально выражать и доказывать свойства систем.
Построенное отображение позволяет использовать существующие средства поддержки языка AMN для автоматической генерации теорем, которые утверждают, что система интеграции данных, основанная на RDF, осуществляет корректную интеграцию данных из некоторого набора источников. Эти теоремы затем автоматизированно доказываются с использованием инструментария доказательства.
Для повышения практичности метода верификации исследователи разработали программный подход к его реализации. Они использовали различные инструменты, такие как OWL API, Xtext и Atlas Transformation Language (ATL), для автоматического преобразования схем данных, запросов и представлений в спецификации AMN.
Этот подход позволяет пользователям применять метод верификации к реальным задачам интеграции данных, накопленных в исследовательских инфраструктурах, в различных областях, таких как здравоохранение, умное землепользование, финансовое моделирование, астрономия и других.
Новый метод автоматизированной верификации обеспечивает ряд преимуществ, включая значительное сокращение времени и усилий, необходимых для проверки корректности интеграции; повышенная уверенность пользователей в правильности и целостности интегрированных данных.
«Наш новый метод верификации предлагает высокий уровень автоматизации при формальной проверке корректности интеграции данных, — сказал ведущий специалист лаборатории открытых информационных технологий Сергей Ступников. — Это поможет исследователям и другим пользователям получать более достоверные результаты при работе с интегрированными научными данными».
Поделиться