Рассмотрено развитие методики формальной верификации свойств мультимодальных интеллектуальных интерфейсов, обеспечивающих естественное интуитивное взаимодействие информационных систем с человеком. В качестве языка для решения задач формальной верификации интерфейсов выбрана логика тайлов, а в качестве языка для формулировки этих свойств - временная модальная логика. Обоснован такой выбор, рассмотрены принципы верификации (доказательства) свойств интерфейсов как проверки правильности взаимодействия агентов в мультиагентной системе. Автоматизацию проверки правильности взаимодействия предложено осуществлять логическими программами, получаемыми в результате перехода от описания свойств интерфейсов в логике тайлов и требований правильности взаимодействия на языке модальной логики к программе проверки правильности на языке логического программирования Visual Prolog. Методика формальной верификации свойств мультимодальных интеллектуальных интерфейсов проиллюстрирована на примере получения описания поведения агентов в логике тайлов, свойства обязательной реакции в модальной логике и логической программой для случая трех взаимодействующих агентов (руководителя и двух исполнителей). Рассмотрены перспективы использования предлагаемой методики для других свойств и приложений.
