Application of formal methods in the design of a single window system
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.
References
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
Copyright (c) 2021 Journal of the Belarusian State University. Mathematics and Informatics
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.
The authors who are published in this journal agree to the following:
- The authors retain copyright on the work and provide the journal with the right of first publication of the work on condition of license Creative Commons Attribution-NonCommercial. 4.0 International (CC BY-NC 4.0).
- The authors retain the right to enter into certain contractual agreements relating to the non-exclusive distribution of the published version of the work (e.g. post it on the institutional repository, publication in the book), with the reference to its original publication in this journal.
- The authors have the right to post their work on the Internet (e.g. on the institutional store or personal website) prior to and during the review process, conducted by the journal, as this may lead to a productive discussion and a large number of references to this work. (See The Effect of Open Access.)