Разработка процессов синхронизации моделей и принципов проверки их корректности
9
иные свойства могут быть исключены как лишние или излишне стро-
гие, а влияние некоторых может быть учтено в меньшей степени [6].
Далее требуется определить, какие задачи стоят перед создаваемым
модулем синхронизации и какое качество процесса синхронизации
должно быть в итоге достигнуто. В зависимости от этого выбирается
тип архитектуры системы синхронизации, а также дополнительные
компоненты, взятые в зависимости от параметров системы.
Примеры процессных программ синхронизации и проверки
их корректности на языке ПРОЛОГ.
Как было отмечено, важную
роль в создании процессов синхронизации моделей играет их вери-
фикация. Используя полученные формальные выражения для свойств
корректности синхронизации, а также определяя процессное пред-
ставление данной процедуры, можно составить тестовую программу
проверки корректности процесса синхронизации на одном из языков
логического программирования.
Рассмотрим простейшую синхронизацию как совокупность двух
не взаимодействующих друг с другом процессов, каждый из которых
работает с одной из моделей, определенным образом изменяя ее со-
стояние (рис. 3).
a
1
a
2
a
3
?y
1
?y
2
b
1
b
2
b
3
b
4
?x
1
?x
1
?x
2
A
B
Рис. 3.
Представление синхронизации моделей в виде двух параллельных
процессов
А
и
В
Представим эти процессы в виде логической программы (листинг
1) на языке ПРОЛОГ в версии SWI PROLOG [15]. Каждый переход
процессов в этой программе представлен фактом, начинающимся с
предикатного символа
transform
, отношение консистентности между
моделями представлено перечислением пар состояний моделей, по
достижении которых будем считать, что процесс синхронизации
успешно завершен. Правила достижимости состояний каждого про-
цесса представлены правилами, начинающимися с предикатов
acces-
sible
.
