Аннотация:
Динамические реконфигурирования могут изменять архитектуру компонентно-ориентированных систем, не подвергаясь никакому системному простою. В этом контексте основной вклад данной статьи — доказательство результатов корректности реконфигурирования систем, используя графовые грамматики. В этой статье предложены новые охраняемые реконфигурирования на базе логики Хоара, которые построены на основе примитивных операций по реконфигурированию и включают последовательности реконфигурирований, альтернативные и повторяющиеся конструкции, сохраняя при этом непротиворечивость конфигураций. Практический вклад состоит в описании имплементации компонентно-ориентированной модели, используя программный инструмент GROOVE для преобразования графов. После обогащения модели интерпретированными конфигурациями и реконфигурированиями, совместимого с непротиворечивостью, отношение симуляции используется для доказательства корректности имплементации, выполненной под GROOVE. Эта имплементация иллюстрирована на примере многоуровневого облачно-ориентированного приложения.
Ключевые слова:компонентно-ориентированные системы, динамическое реконфигурирование, непротиворечивость, соответствие, реализация, GROOVE.