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