10 / 23
74
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. «Приборостроение». 2016. № 3
Действиями
i
-го исполнителя являются:
1)
поместить
сообщение
в выходной канал
ИiР
Иi-Поместить
(
ИiР
(
сообщение
));
2)
получить
сообщение
из входного канала
PИi
Иi-Получить
((
PИi
(
сообщение
)).
Аналогично описанию поведения руководителя каждый исполни-
тель может вести себя в соответствии с перечисленными ниже секвен-
тами.
И
i
-Подготовка
:
(
(
))
.
(
(
))
Иi-Поместить ИiР открыт
Иi-Получить РИi приглашение
-
Иi Готов
Иi -Приглашен
И
i
-Реакция:
(
(
))
(
(
))
Иi-Получить РИi приглашение
.
Иi Поместить ИiР приглаш
-
ен
Иi -Приглашен
Иi -Принято
И
i
-Уведомление:
-
(
)
.
-
(
(
)
(
)
)
Иi
Иi Получить Р
Поместить И
Иi задани
iР приглаш н
е
е
-
-
Иi Принято
Иi Управление
И
i
-Информирование:
-
(
(
))
-
.
-
(
)
(
)
Иi Получить РИi задание
Иi Поместить ИiР согласен
-
Иi Управление
Иi Выполнено
Иi
-Завершение:
-
(
)
-
.
-
(
(
)
(
)
)
Иi
Иi Получить Р
Поместить ИiР со
Иi ожидани
гл ен
е
ас
-
Иi Выполнено
Иi Завершено
И
i
-Закрытие:
-
(
(
))
.
-
(
(
))
Иi Получить РИi ожидание
Иi Поместить ИiР закрыт
-
-
Иi Завершено
Иi Закрыт
Формулировка свойств интеллектуального интерфейса на язы-
ке модальной логики.
Для формулировки требуемых свойств интел-
лектуальных интерфейсов в работе [1] предложено использовать широ-
ко применяемый для подобных целей язык временнóй модальной логи-
ки. Этот язык хорошо изучен и его применение для верификации также
широко известно, в настоящей статье не будем уделять ему слишком
много внимания. Рассмотрим принципы формулировки свойств интел-
лектуальных интерфейсов с привязкой к понятиям тайлов (секвентов),
с помощью операций над которыми эти свойства будут проверяться.
В качестве примера одного из таких свойств выберем простейшее свой-
ство обязательной реакции.
Суть этого свойства применительно к взаи-