Разработка процессов синхронизации моделей и принципов проверки их корректности
1
УДК 004.413
Разработка процессов синхронизации моделей
и принципов проверки их корректности
© В.В. Девятков, Д.В. Ошкало
МГТУ им. Н.Э. Баумана, Москва, 105005, Россия
Изложены новые принципы решения задачи синхронизации моделей на основе фор-
мального процессного описания механизмов синхронизации и свойств их коррект-
ности, формализуемых на языке временной модальной логики с последующей про-
веркой этих свойств с использованием логического вывода. Рассмотрены основные
свойства, обеспечивающие корректность процесса синхронизации моделей, а
также особенности создания систем синхронизации.
Ключевые слова:
синхронизация моделей, трансформация моделей, свойства кор-
ректности, процессы, модальная логика.
Введение.
Моделеориентированный подход к разработке про-
граммного обеспечения предполагает использование множества
формальных структурированных компонентов — моделей — с целью
автоматизированного построения на их основе различных артефак-
тов — программного кода, документации, конфигурации и др. Ис-
пользуя подобный подход, разработчик избавляется от рутинной ра-
боты по написанию шаблонов и заготовок кода, созданию конфигу-
рационных файлов и скриптов и т. п.
Однако при использовании моделеориентированного подхода на
плечи разработчика ложится ряд других задач, связанных с создани-
ем и сопровождением моделей, количество и разнообразие которых в
зависимости от сложности проекта может быть значительным: моде-
ли требований, архитектуры компонентов, сценарии использования,
модели данных и т. д. Зачастую эти модели так или иначе связаны
друг с другом. Они могут разрабатываться отдельно, но при этом
быть семантически идентичными или характеризовать с разных по-
зиций один и тот же проект. Например, это могут быть различного
рода концептуальные модели проекта [1] или модели, полученные на
основе других моделей посредством трансформации, это может быть
схема реляционной базы данных, созданная на основе диаграммы
классов UML [2].
Механизмом синхронизации моделей, или просто синхронизаци-
ей, обычно называют механизм, имеющий дело с двумя моделями и
осуществляющий внесение изменений в одну модель при изменениях
в другой с сохранением корректности синхронизации. Понятие кор-
