Application of formal methods in the design of a single window system

  • Raman E. Sharykin Belarusian State University, 4 Niezaliežnasci Avenue, Minsk 220030, Belarus

Abstract

This paper proposes an approach that demonstrates the development of single window document circulation systems at the early stage of their design, based on the use of formal methods in the specification of a system, the specification of metrics for its analysis and the estimation of metrics values. An example of a single window document circulation system is modeled formally within the framework of the distributed object-based stochastic hybrid systems (DOBSHS) model using the SHYMaude specification language. Several metrics are proposed to evaluate the system. These metrics are specified formally using the QuaTEx language. The system is analyzed statistically using the MultiVeStA tool, which analyzes a single window document circulation system, represented as a rewriting logic Maude specification obtained by the translation of the SHYMaude system specification. In the process of the statistical analysis, the number of employees required for the effective system functioning is determined. The resulting value is used as a starting value in an extended system, in which there is an officer number management maintaining the length of the application queue in the desired range. A statistical study of the extended system reveals a drawback that is eliminated by adjusting the system, showing how this approach can be used to study and refine systems of this type at the early stage of designing the system model itself.

Author Biography

Raman E. Sharykin, Belarusian State University, 4 Niezaliežnasci Avenue, Minsk 220030, Belarus

competitor at the department of software engineering, faculty of applied mathematics and computer science

References

  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.
Published
2021-04-12
Keywords: mathematical modelling, stochastic systems, statistical analysis, model specification, document circulation, single window systems
How to Cite
Sharykin, R. E. (2021). Application of formal methods in the design of a single window system. Journal of the Belarusian State University. Mathematics and Informatics, 1, 79-90. https://doi.org/10.33581/2520-6508-2021-1-79-90
Section
Theoretical Foundations of Computer Science