Применение формальных методов при проектировании системы одного окна

  • Роман Евгеньевич Шарыкин Белорусский государственный университет, пр. Независимости 4, 220030, г. Минск, Беларусь
DOI: https://doi.org/10.33581/2520-6508-2021-1-79-90

Аннотация

Предлагается подход, демонстрирующий разработку систем документооборота по принципу одного окна на раннем этапе их проектирования, основанный на применении формальных методов в части спецификации системы и метрик ее анализа, а также оценки значений метрик. Пример системы одного окна моделируется формально в рамках модели распределенных объектно ориентированных стохастических гибридных систем (РООСГС) с помощью языка спецификации SHYMaude. Предлагаются несколько метрик, позволяющих оценить систему. Данные метрики специфицируются формально посредством языка QuaTEx. Система одного окна, представленная как спецификация переписывающей логики Maude, полученная трансляцией спецификации SHYMaude, анализируется статистически с помощью инструмента MultiVeStA. В процессе статистического анализа определяется количество сотрудников, необходимое для эффективного функционирования системы. Полученное значение используется как стартовое значение в расширенной системе, в которой присутствует управление количеством сотрудников в целях поддержания длины очереди пакетов документов в желаемом диапазоне. При статистическом исследовании расширенной системы обнаруживается недостаток, который устраняется доработкой системы, что показывает, как данный подход может быть использован для изучения и доработки систем подобного типа на раннем этапе построения самой модели системы.

Биография автора

Роман Евгеньевич Шарыкин, Белорусский государственный университет, пр. Независимости 4, 220030, г. Минск, Беларусь

соискатель кафедры технологий программирования факультета прикладной математики и информатики. Научный руководитель – доктор технических наук, профессор А. Н. Курбацкий

Литература

  1. Krasnyanskii MN, Karpushkin SV, Ostroukh AV, Obukhov AD, Kasatonov IS, Bukreev DV, et al. Proektirovanie informatsionnykh sistem upravleniya dokumentooborotom nauchno-obrazovatel’nykh uchrezhdenii [Design of information systems for document management of scientific and educational institutions]. Tambov: Publishing house of FSBEI HPE «TSTU»; 2015. 216 p. Russian.
  2. Sharykin RE, Kourbatski AN. Verification of distributed object-oriented stochastic hybrid systems. Vesnik Grodzenskaga dzjarzhawnaga wniversitjeta imja Janki Kupaly. Seryja 2. Matjematyka. Fizika. Infarmatyka, vylichal’naja tjehnika i kiravanne. 2019;9(3):123–132. Russian.
  3. Sharykin RE, Kourbatski AN. A model of distributed objectbased stochastic hybrid systems. Journal of the Belarusian State University. Mathematics and Informatics. 2019;2:52–61. Russian.
  4. Clavel M, Durán F, Eker S, Lincoln P, Martı́-Oliet N, Meseguer J, et al. Maude: specification and programming in rewriting logic. Theoretical Computer Science. 2002;285(2):187–243. DOI: 10.1016/S0304-3975(01)00359-0.
  5. Sharykin RE. SHYMaude specification of a single window document circulation system [Internet]. GitHub Inc., 2021 [cited 2020 November 1]. Available from: https://github.com/shymaude/singleWindow.
  6. Sen K, Viswanathan M, Agha G. On statistical model checking of stochastic systems. In: Etessami K, Rajamani SK, editors. Computer aided verification. Proceedings of the 17th International conference; 2005 July 6–10; Edinburgh, Scotland, UK. Berlin: Springer-Verlag; 2005. p. 266–280. (Lecture notes in computer science; volume 3576). DOI: 10.1007/11513988_26.
  7. Vandin A, Sebastio S. MultiVeStA: statistical model checking for discrete event simulators. In: Buchholz P, Cortellessa V, Horvath A, Muscariello L, Squillante M, editors. Proceedings of the 7th International conference on performance evaluation methodologies and tools; 2013 December 10–12; Torino, Italy. Brussels: Institute for Computer Sciences, Social Informatics and Telecommunications Engineering; 2013. p. 310–315. DOI: 10.4108/icst.valuetools.2013.254377.
  8. Agha G, Meseguer J, Sen K. PMaude: rewrite-based specification language for probabilistic object systems. Electronic Notes in Theoretical Computer Science. 2006;153(2):213–239. DOI: 10.1016/j.entcs.2005.10.040.
Опубликован
2021-04-12
Ключевые слова: математическое моделирование, стохастические системы, статистический анализ, спецификация моделей, документооборот, системы одного окна
Как цитировать
Шарыкин, Р. Е. (2021). Применение формальных методов при проектировании системы одного окна. Журнал Белорусского государственного университета. Математика. Информатика, 1, 79-90. https://doi.org/10.33581/2520-6508-2021-1-79-90
Выпуск
№ 1 (2021): Журнал Белорусского государственного университета. Математика. Информатика
Раздел
Теоретические основы информатики

Copyright (c) 2021 Журнал Белорусского государственного университета. Математика. Информатика

Лицензия Creative Commons

Это произведение доступно по лицензии Creative Commons «Attribution-NonCommercial» («Атрибуция — Некоммерческое использование») 4.0 Всемирная.

Авторы, публикующиеся в данном журнале, соглашаются со следующим:

  1. Авторы сохраняют за собой авторские права на работу и предоставляют журналу право первой публикации работы на условиях лицензии Creative Commons Attribution-NonCommercial. 4.0 International (CC BY-NC 4.0).
  2. Авторы сохраняют право заключать отдельные контрактные договоренности, касающиеся неэксклюзивного распространения версии работы в опубликованном здесь виде (например, размещение ее в институтском хранилище, публикацию в книге) со ссылкой на ее оригинальную публикацию в этом журнале.
  3. Авторы имеют право размещать их работу в интернете (например, в институтском хранилище или на персональном сайте) до и во время процесса рассмотрения ее данным журналом, так как это может привести к продуктивному обсуждению и большему количеству ссылок на данную работу. (См. The Effect of Open Access).