Верификация свойств интеллектуальных интерфейсов в логике тайлов

ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. «Приборостроение». 2016. № 3

DOI: 10.18698/0236-3933-2016-3-65-87

УДК 004.5

Верификация свойств интеллектуальных

интерфейсов в логике тайлов

В.В. Девятков

МГТУ им. Н.Э. Баумана, Москва, Российская Федерация

e-mail:

Рассмотрено развитие методики формальной верификации свойств мультимо-

дальных интеллектуальных интерфейсов, обеспечивающих естественное инту-

итивное взаимодействие информационных систем с человеком. В качестве язы-

ка для решения задач формальной верификации интерфейсов выбрана логика

тайлов, а в качестве языка для формулировки этих свойств — временнáя мо-

дальная логика. Обоснован такой выбор, рассмотрены принципы верификации

(доказательства) свойств интерфейсов как проверки правильности взаимодей-

ствия агентов в мультиагентной системе. Автоматизацию проверки правиль-

ности взаимодействия предложено осуществлять логическими программами,

получаемыми в результате перехода от описания свойств интерфейсов в логике

тайлов и требований правильности взаимодействия на языке модальной логики

к программе проверки правильности на языке логического программирования

Visual Prolog. Методика формальной верификации свойств мультимодальных

интеллектуальных интерфейсов проиллюстрирована на примере получения опи-

сания поведения агентов в логике тайлов, свойства обязательной реакции в мо-

дальной логике и логической программой для случая трех взаимодействующих

агентов (руководителя и двух исполнителей). Рассмотрены перспективы ис-

пользования предлагаемой методики для других свойств и приложений.

Ключевые слова:

свойства интеллектуальных интерфейсов, логика тайлов, мо-

дальная логика, верификация свойств, интеллектуальные агенты, язык логиче-

ского программирования Visual Prolog.

Verification of Intelligent Interface Properties

in the Tiles Logic

V.V. Devyatkov

Bauman Moscow State Technical University, Moscow, Russian Federation

e-mail:

In this work we developed the methodology for formal verification of properties

of multimodal intelligent interfaces, providing a natural intuitive interaction

of information systems with the person. We selected the tiles logic as the language for

solving problems of formal verification of interfaces and temporal modal logic as the

ИНФОРМАТИКА,

ВЫЧИСЛИТЕЛЬНАЯ ТЕХНИКА

И УПРАВЛЕНИЕ