17 / 23
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. «Приборостроение». 2016. № 3
81
sequentRp2p(XP222, S1P22, rp2p(p2receive(lp22(M1L22)),
p2put(p2l2(M2L22))), S2P22)
XP222 = p2reaction, S1P22 = p2invited, M1L22 = invitation,
M2L22 = invited, S2P22 = p2accepted
======================================================
XL11=preparation, XP111=p1preparation, XP221=p2preparation,
XL12=reaction, XP112=p1reaction, XP222=p2reaction
1 Solution
Заключение.
Кратко изложены принципы создания методики фор-
мальной верификации свойств мультимодальных интеллектуальных ин-
терфейсов на основе использования логики тайлов, временнóй модаль-
ной логики и логического программирования. Методика формальной
верификации свойств мультимодальных интеллектуальных интерфейсов
проиллюстрирована на примере проверки свойства обязательной реак-
ции простейшей системы, состоящей из трех агентов. В этом случае для
проверки свойства обязательной реакции достаточно использования па-
раллельной композиции секвентов. Для верификации свойств мульти-
модальных интеллектуальных интерфейсов больших и сложных систем
требуется представлять систему как иерархическое множество незави-
симых процессов (агентов) и каналов связи между этими процессами,
которые могут реконфигурироваться. Логика тайлов в наибольшей
степени подходит для верификации свойств мультимодальных интел-
лектуальных интерфейсов больших и сложных систем, поскольку ин-
терфейсы являются базовыми объектами, которыми эта логика способна
манипулировать. Различные схемы соединений интерфейсов могут со-
здаваться в логике тайлов вследствие параллельной и горизонтальной
композиций, порождающих различные системные конфигурации. Каж-
дая такая конфигурация задает пространственное представление общего
состояния системы, состоящего из локальных состояний. Горизонталь-
ная или параллельная композиция также обеспечивает возможность
представления контекстной зависимости данных вследствие наличия
интерфейсов. Поведение системы в целом определяется множеством
тайлов, задающих локальные изменения конфигураций системы, кото-
рые являются локальными состояниями системы, в результате верти-
кальной композиции. Для того чтобы изложенное выше было более по-
нятным, введем следующие обозначения и рассмотрим пример.
Архитектуру интерфейсной системы любого уровня иерархии пред-
ставим четверкой
S =
{
P
,
L
,
I
,
O
}, где
P
— множество
процессов систе-
мы, изображаемых прямоугольниками;
L
— множество каналов системы,
соединяющих процессы;
I —
множество подмножеств
I
(
p
)
L
входных
каналов процессов
p
P
;
O —
множество подмножеств
O
(
p
)
L
выход-
ных каналов процесса
p
P.