Verification of Intelligent Interface Properties in the Tiles Logic

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 the 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 transition from the agents interaction description in the tiles logic and requirements to proper interaction in modal logic language to the validation program in logic programming language Visual Prolog. The methodology for formal verification of properties 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.

References

[1] Devyatkov V.V., Alfimtsev A.N. Necessary and sufficient formal properties of multimodal interface. Vestn. Mosk. Gos. Tekh. Univ. im. N.E. Baumana, Priborostr., Spetsvyp. "Informatsionnye tekhnologii i komp’yuternye sistemy" [Herald of the Bauman Moscow State Tech. Univ., Instrum. Eng., Spec. Issue "Information technology and computer system"], 2011, pp. 159-166 (in Russ.).

[2] Robin M. Communicating and Mobile Systems: The п-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, pp. 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, PP. 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, pp. 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, pp. 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), 2007, July 22-25, pp. 123-128.

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

[9] Adamenko A.N., Kuchkov A. Logicheskoe programmirovanie i Visual Prolog [Logic Programming and Visual Prolog]. St. Petersburg, BKhV-Petersburg Publ., 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), no. 1, pp. 288-308.