Verification of Knowledge Obtained in the Study of Business Process Models

The paper focuses on the method of formal verification of knowledge obtained in the study of business process models. As a formal language for the presentation and verification of business processes, a certain version of π-calculus was chosen, and linear temporal modal logic was chosen as a language for formulating test assignments, i.e., questions, to be checked. The paper gives the rationale for such choice, and considers the principles of developing the test assignments in the language of modal logic and their usage for knowledge verification. The study proposes to automate knowledge testing with logic programs obtained as a result of the transition from a description of business processes to a verification program in the logical programming language Visual Prolog. The formal knowledge verification technique is illustrated by examples of knowledge verification. Findings of research show how the transition from the description of business processes to the procedures of formal verification of knowledge is carried out. The prospects for the development of the proposed method are discussed

This work was supported by the Ministry of Education and Science of the Russian Federation (project no. 2.5048.2017/8.9)

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. [Herald of the Bauman Moscow State Tech. Univ., Instrum. Eng.], 2011, spec. iss "Information technology and computer systems", pp. 159--167 (in Russ.).

[2] Robin M. Communicating and mobile systems: the п-calculus. Cambridge University Press, 2003.

[3] Medvidovic N., Taylor R.M. A classification and comparison framework for software architecture description languages. IEEE Trans. Softw. Eng., 2000, vol. 26, no. 1, pp. 70--93. DOI: https://doi.org/10.1109/32.825767

[4] Braga C., Sztajnberg A. Towards a rewriting semantics for a software architecture description language. Electron. Notes Theor. Comput. Sc., 2004, vol. 95, pp. 149--168. DOI: https://doi.org/10.1016/j.entcs.2004.04.010

[5] Bruni R., Fiadeiro J.L., Lanese I., et al. New insight into the algebraic properties of architectural connectors. IFIP TCS, 2004, vol. 155, pp. 367--380. DOI: https://doi.org/10.1007/1-4020-8141-3_29

[6] Choutri A., Belala F., Barkaoui K. A tile logic based approach for software architecture description analysis. JSEA, 2010, vol. 3, no. 11, pp. 1067--1079. DOI: http://dx.doi.org/10.4236/jsea.2010.311126

[7] Bouanaka C., Choutri A., Belala F. On generating tile system for a software architecture: case of a collaborative application session. ICSOFT2007, 2007, pp. 123--128.

[8] Bog A. A visual environment for the simulation of business processes based on the Pi-calculus. Master Thesis. Potsdam University, 2006.

[9] Devyatkov V.V. Construction, optimization, and modification of processes. Vestn. Mosk. Gos. Tekh. Univ. im. N.E. Baumana, Priborostr. [Herald of the Bauman Moscow State Tech. Univ., Instrum. Eng.], 2012, no. 4, pp. 60--79 (in Russ.).

[10] Kleene S.C. Representation of events in nerve nets and finite automata. In: Automata studies. Princeton University Press, 1956, pp. 3--42.

[11] Wooldridge M. An introduction to multiagent systems. John Wiley & Sons, 2009.

[12] Devyatkov V.V., Rumbesht V.V. Situational modal fuzzy calculus for analysis of complex objects. Vestn. Mosk. Gos. Tekh. Univ. im. N.E. Baumana, Priborostr. [Herald of the Bauman Moscow State Tech. Univ., Instrum. Eng.], 2001, no. 3, pp. 3--18 (in Russ.).

[13] Lemmon E. Algebraicheskaya semantika dlya modal’nykh logik I. II [Algebraic semantics for modal logic I. II]. V: Semantika modal’nykh i intensional’nykh logic [In: Semantics of modal and intensional logics]. Moscow, Progress Publ., 1981.

[14] Adamenko A.N., Kuchkov A. Logicheskoe programmirovanie i Visual Prolog [Logic programming and Visual Prolog]. St. Petersburg, BKhV--Peterburg Publ., 2003.

[15] Devyatkov V.V. Verification of intelligent interface properties in the tiles logic. Vestn. Mosk. Gos. Tekh. Univ. im. N.E. Baumana, Priborostr. [Herald of the Bauman Moscow State Tech. Univ., Instrum. Eng.], 2016, no. 3, pp. 65--87 (in Russ.). DOI: http://dx.doi.org/10.18698/0236-3933-2016-3-65-87