ИСТИНА

На настоящее время значительная часть информационно-аналитических систем построена на основе так называемых веб-фреймворков — программных библиотек, реализующих стандартную архитектуру веб-приложений. В рамках такой стандартной архитектуры, данные системы хранятся в базе данных (БД), доступ к которой производится с использованием языка SQL. Согласно открытой статистике статистике по технологиям, используемым при разработке 1000 наиболее активно используемых информационных систем, для разработки основного кода системы чаще всего используются языки программирования с динамической типизацией, такие как: Python, Ruby, JavaScript или PHP. Для сложных информационно-аналитических систем, например, для социальных сетей, графовая модель данных допускает более компактное описание предметной области, чем реляционная, используемая в современных системах управления базами данных. В этой связи, на практике в таких системах обычно используются средства трансляции между графовой или объектной моделью в основном коде системы и реляционной моделью данных в БД. При разработке систем согласно стандартной архитектуре, верификация, как правило затруднена в связи с целым рядом факторов, включая следующие: динамическая типизация языка программирования не позволяет выполнять ряд проверок на этапе компиляции; работоспособность кода сложной системы зависит не только от структуры, но и от содержания БД; код, использующие графовые отношения транслируется в запросы на языке SQL зачастую некорректно или с непредсказуемой производительностью; для решения нетривиальных задач возникает необходимость использования дополнительного SQL-кода или нестандартных генераторов SQL-кода. В рамках общего подхода к верификации крупных программных комплексов на основе подхода с использованием предметно-ориентированных языков с заданной формальной семантикой для устранения перечисленных факторов предлагается разработать формальную модель, допускающую описание целевой модели данных. В терминах этой модели могут быть представлены как отдельные SQL-запросы, так и процессы работы генераторов SQL-кода. После трансляции в термины общей формальной модели, могут быть выделены спецификации системы с позиций выполняемых запросов к БД, и проведён реинжиниринг на основе этой спецификации в языки, адекватно отражающие специфику предметной области целевой информационно-аналитической системы. Исследования проводятся при частичной поддержке гранта РФФИ 16-07-01178а.