2 / 23
66
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. «Приборостроение». 2016. № 3
language for formulating these properties. The article explains the choice, considers
the principles of verification (proof) of the interfaces properties as the validation
of the agents interaction in the multi-agent system. To automate the validation
of the agents interaction, we use the logic programs obtained as a result of the transi-
tion from the agents interaction description in the tiles logic and requirements to
proper interaction in modal logic language to the validation program in logic pro-
gramming language Visual Prolog. The methodology for formal verification of proper-
ties of multimodal intelligent interfaces is illustrated by the description of the agents
behavior in the tiles logic, interfaces properties in the modal logic and logic program
in the case of the three interacting agents (the leader and two executors). Of particular
interest are the prospects of using the proposed methodology for other properties and
applications.
Keywords:
intelligent interface properties, tiles logic, modal logic, verification
of properties, intelligent agents, logic programming language Visual Prolog.
Введение.
Свойства мультимодальных интеллектуальных интер-
фейсов, реализация которых
обеспечивает естественное «безбарьерное»
взаимодействие пользователя с машиной,
рассмотрены в работе [1].
Какие из этих свойств необходимо воплощать, зависит от конкретной
системы, где требуется соответствующий интерфейс. В любом случае,
если какое-либо свойство интерфейса должно быть реализовано, то,
во-первых, требуется его точная спецификация, а во-вторых, возмож-
ность формальной проверки этой спецификации применительно к ин-
терфейсу конкретной системы. Поскольку речь идет о программной си-
стеме, упомянутая спецификация свойств интерфейса и их формальная
проверка могут рассматриваться как специфическая область верифика-
ции программных систем в целом. В настоящее время существует три
основных подхода к верификации программных систем: 1) тестирование
наличия у системы требуемых свойств; 2) формальное доказательство
наличия свойств в рамках некоторого исчисления; 3) моделе-ориен-
тированное доказательство наличия свойств. Различие этих подходов
заключается в следующем.
Тестирование наличия у системы требуемых свойств.
При те-
стировании на вход модели подаются заранее подготовленные и пред-
ставленные в каком-либо языке последовательности действий (воспри-
ятий и реакций агентов) и проверяется, проявляет ли модель ожидае-
мые свойства. Недостаток тестирования: мощность множества тести-
рующих последовательностей действий (нитей) может быть слишком
велика, что приводит к комбинаторному взрыву и вычислительным
проблемам тестирования. Кроме того, множество тестирующих после-
довательностей формируется экспертом и нет никакой гарантии пол-
ноты этого множества для верификации.
Формальное доказательство наличия свойств в рамках некото-
рого исчисления.
При формальном доказательстве эти свойства форму-
лируются в виде теорем (целей) на языке соответствующего исчисления,
которые затем доказываются (выводятся) из начальных знаний (аксиом),
представленных на том же языке с использованием специальных правил