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

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

Литература

[1] Девятков В.В., Алфимцев А.Н. Необходимые и достаточные формальные свойства мультимодального интерфейса // Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. Спец. вып. "Информационные технологии и компьютерные системы". 2011. С. 159-166.

[2] Robin M. Communicating and Mobile Systems: The pi-calculus. Cambridge: University Press, 2003. 159 р.

[3] Medvidovic N., Taylor R.M. A Classification and comparison framework for software architecture description languages // IEEE Transactions on Software Engineering. 2000. Vol. 26. No 1. Р. 70-93.

[4] Braga C., Sztajnberg A. Towards a rewriting semantics for a software architecture description language // Proceedings of WMF 2003, 6th Workshop on Formal Methods, Campina Grande, Brazil, E.N.T.C.S. 95. 2003. Р. 148-168.

[5] Bruni R., Fiadeiro J.L., Lanese I., Lopes A., Montanari U. New insight into the algebraic properties of architectural connectors // International Federation for Information Processing. 2004. Vol. 155. P. 367-380.

[6] Choutri A., Belala F., Barkaoui K. A Tile logic based approach for software architecture description analysis // J. Software Engineering & Applications. 2010. Vol. 3. Р. 1067-1079.

[7] Bouanaka C., Choutri A., Belala F. On Generating tile system for a software architecture: case of a collaborative application session // ICSOFT2007 (Second Conference on Software and Data Technologies), July 22-25. 2007. Р. 123-128.

[8] Bruni R. Tile logic for synchronized rewriting of concurrent systems. Phd Thesis. University of Pisa. TD-1/99. March. 1999.

[9] Адаменко А.Н., Кучков А. Логическое программирование и Visual Prolog. СПб.: БХВ-Петербург, 2003.

[10] Bouanaka C., Belala F., Barkaoui K. A Tile logic based semantics for mobile software architectures // International Journal of Critical Computer-Based Systems. 2011. Vol. 2(3). Р. 288-308.