Верификация знаний, полученных при изучении моделей бизнес-процессов

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

Работа поддержана грантом Минобрнауки России № 2.5048.2017/8.9

Литература

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

[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] Девятков В.В. Построение, оптимизация и модификация процессов. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение, 2012, № 4, с. 60--79.

[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] Девятков В.В., Румбешт В.В. Нечеткое модальное ситуационное исчисление для анализа сложных объектов. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение, 2001, № 3, с. 3--18.

[13] Леммон E. Алгебраическая семантика для модальных логик I. II. В: Семантика модальных и интенсиональных логик. M., Прогресс, 1981.

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

[15] Девятков В.В. Верификация свойств интеллектуальных интерфейсов в логике тайлов. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение, 2016, № 3, с. 65--87. DOI: http://dx.doi.org/10.18698/0236-3933-2016-3-65-87