Разработка процессов синхронизации моделей и принципов проверки их корректности
7
сделано. Данное утверждение касается обеих синхронизируемых мо-
делей:
{
(
?s
,
?t
)
◊
[
(
!s
,
!t
)
(
?t ≡ !t
)
(
?s ≡ !s
)
]
}
.
Симметричность.
Данное свойство лежит в основе принципа
равноправия моделей по отношению к процессу синхронизации: ре-
зультат синхронизации не должен зависеть от порядка обработки мо-
делей:
{
[
(
?s
,
?t
)
(
?s’
,
?t’
)
(
?s ≡ ?t’
)
(
?t ≡ ?s’
)
]
◊
[
(
!s
,
!t
)
(
!s’
,
!t’
)
(
!s ≡ !t’
)
(
!t ≡ !s’
)
]
}
.
Возможность отката изменений.
Это требование проявляется в
следующем сценарии. Исходная модель была модифицирована, и
связанные с ней изменения были перенесены в целевую модель, та-
ким образом обе модели стали консистентными. После этого измене-
ния в первой модели были отменены, она вернулась к своему перво-
начальному состоянию. В этом случае целевая модель также должна
вернуться к своему первоначальному состоянию:
{
[
(
?s
,
?t
)
[
(
!s’
,
!t’
)
((
?s’ ≡ ?s
)
(
?t’ ≡ ?t
))
]
◊
[
(
!s’ ≡ ?s
)
(
!t’ ≡ ?t
)
]
}.
Принцип Гиппократа.
Изменения, вносимые процессом син-
хронизации в структуру моделей, должны быть минимальными среди
тех, что приведут модели к консистентному состоянию. Стабиль-
ность и возможность отката изменений являются частными формами
данного принципа.
Принципы создания процессных программ синхронизации и
проверки их корректности.
Помимо обозначенных свойств кор-
ректности, которым должен удовлетворять процесс синхронизации
моделей, можно выделить более частные свойства, обусловленные
той или иной предметной областью, напрямую влияющие на внут-
реннюю логику процесса синхронизации. В работе [14] приведены
возможные примеры систем синхронизации в зависимости от следу-
ющих критериев:
1. Гомогенность или гетерогенность синхронизируемых моделей.
Гомогенными являются модели, состоящие из одних и тех же струк-
турных элементов и построенные по одним и тем же правилам (т. е.
однотипные модели). В противном случае модели являются гетеро-
генными (разнородными).
2. Однонаправленность или двунаправленность трансформаций.
В зависимости от назначения может осуществляться как однонаправ-
