4 / 23
68
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. «Приборостроение». 2016. № 3
каких-либо свойств информационных систем на основе логик тайлов из-
вестны достаточно давно [8]. Для того чтобы логику можно было ис-
пользовать для того или иного приложения, необходимо создать множе-
ство тайлов, соответствующих этому приложению.
В рассматриваемом случае приложением является проверка (дока-
зательство) свойств интеллектуальных интерфейсов. Далее будут при-
ведены основные понятия, связанные с тайлами. Затем на простом
примере одного из свойств интеллектуальных интерфейсов, называе-
мым свойством обязательной реакции [1], будет введено необходимое
для примера множество тайлов. Будет показано, как это множество ис-
пользуется для доказательства свойства обязательной реакции, сфор-
мулированного на языке модальной логики. В заключение приведены
направления дальнейших работ в области проверки свойств интеллек-
туальных интерфейсов.
Тайлы и операции над ними.
Достоинства логики тайлов связаны
со структурой ее правил вывода, каждое из которых может быть пред-
ставлено в виде тайла (рис. 1,
а
).
Рис. 1.
Структуры тайла (
а
) и секвента (
б
):
— имя тайла;
?i
i
— начальный входной интерфейс тайла;
?s
i
— начальная конфи-
гурация тайла;
?o
i
—
начальный выходной интерфейс тайла;
!i
o
— конечный вход-
ной интерфейс тайла;
!s
o
— конечная конфигурация тайла;
!o
o
—
конечный выходной
интерфейс тайла;
?a
i
—
восприятие тайла;
!a
o
—
реакция тайла
Тайл позволяет описывать поведение частично определенных ком-
понентов системы, содержащих переменные и называемых конфигура-
циями. Это поведение описывается в терминах возможных взаимодей-
ствий с внешней или внутренней средой. Поведение системы выглядит
как скоординированное взаимодействие отдельных тайлов. Восприятия
и реакции также называют действиями. Интерфейсы тайла задают
форматы его взаимодействия с внешней средой. Тайл
(см. рис. 1,
а
) в
ответ на восприятие
?a
i
задает преобразование начальной конфигура-
ции
?s
i
в конечную конфигурацию
!s
o
, производя реакцию
!a
o
.
Такое
преобразование возможно тогда, когда тайл не только осуществил вос-
приятие
?a
i
, но и когда форматы данных внешней среды тайла удовле-
творяют форматам интерфейсов тайла.
Тайлы, у которых все интерфейсы одинаковы, называют секвента-
ми (рис. 1,
б
). Обозначения интерфейсов в секвентах опускают. Се-
квент обычно изображают не графически, а в следующем виде: