Верифицируемое отображение модели данных, основанной на многомерных массивах, в объектную модель данных

Рассматривается отображение модели данных, основанной на многомерных массивах (ММ-модели), в объектную модель данных. Изложены общие принципы отображения ММ-моделей в объектные модели данных. Рассмотрено отображение конкретной модели — Array Data Model (ADM), использующейся в системе управления базами данных (СУБД) SciDB, в язык СИНТЕЗ, использующийся в качестве канонической модели данных в технологии предметных посредников. Проиллюстрирован метод верификации отображения — доказательства сохранения информации и семантики операций при отображении. Верификация осуществляется при помощи формального языка спецификаций AMN. Практической целью работы ставилось создание базы для виртуальной или материализованной интеграции ресурсов, основанных на многомерных массивах.