Верификация свойств интеллектуальных интерфейсов в логике тайлов | Вестник МГТУ им. Н.Э. Баумана
|

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

Авторы: Девятков В.В. Опубликовано: 15.06.2016
Опубликовано в выпуске: #3(108)/2016  
DOI: 10.18698/0236-3933-2016-3-65-87

 
Раздел: Информатика, вычислительная техника и управление | Рубрика: Системный анализ, управление и обработка информации  
Ключевые слова: свойства интеллектуальных интерфейсов, логика тайлов, модальная логика, верификация свойств, интеллектуальные агенты, язык логического программирования Visual Prolog

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