Treffer: ВЕРИФИКАЦИЯ СВОЙСТВ ИНТЕЛЛЕКТУАЛЬНЫХ ИНТЕРФЕЙСОВ В ЛОГИКЕ ТАЙЛОВ

Рассмотрено развитие методики формальной верификации свойств мультимодальных интеллектуальных интерфейсов, обеспечивающих естественное интуитивное взаимодействие информационных систем с человеком. В качестве языка для решения задач формальной верификации интерфейсов выбрана логика тайлов, а в качестве языка для формулировки этих свойств временнáя модальная логика. Обоснован такой выбор, рассмотрены принципы верификации (доказательства) свойств интерфейсов как проверки правильности взаимодействия агентов в мультиагентной системе. Автоматизацию проверки правильности взаимодействия предложено осуществлять логическими программами, получаемыми в результате перехода от описания свойств интерфейсов в логике тайлов и требований правильности взаимодействия на языке модальной логики к программе проверки правильности на языке логического программирования Visual Prolog. Методика формальной верификации свойств мультимодальных интеллектуальных интерфейсов проиллюстрирована на примере получения описания поведения агентов в логике тайлов, свойства обязательной реакции в модальной логике и логической программой для случая трех взаимодействующих агентов (руководителя и двух исполнителей). Рассмотрены перспективы использования предлагаемой методики для других свойств и приложений ; 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 thelanguage 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 transition from the agents interaction description in the tiles logic and requirements to proper ...