Geodesic
Application of formal methods in the design of a single window system
Journal of the Belarusian State University. Mathematics and Informatics, Tome 1 (2021), pp. 79-90.

Voir la notice de l'article provenant de la source Math-Net.Ru

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 modelled 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 analysed statistically using the MultiVeStA tool, which analyses 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.
Keywords: mathematical modelling; stochastic systems; statistical analysis; model specification; document circulation; single window systems. 
@article{BGUMI_2021_1_a6,
     author = {R. E. Sharykin},
     title = {Application of formal methods in the design of a single window system},
     journal = {Journal of the Belarusian State University. Mathematics and Informatics},
     pages = {79--90},
     publisher = {mathdoc},
     volume = {1},
     year = {2021},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/BGUMI_2021_1_a6/}
}
TY  - JOUR
AU  - R. E. Sharykin
TI  - Application of formal methods in the design of a single window system
JO  - Journal of the Belarusian State University. Mathematics and Informatics
PY  - 2021
SP  - 79
EP  - 90
VL  - 1
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/BGUMI_2021_1_a6/
LA  - ru
ID  - BGUMI_2021_1_a6
ER  - 
%0 Journal Article
%A R. E. Sharykin
%T Application of formal methods in the design of a single window system
%J Journal of the Belarusian State University. Mathematics and Informatics
%D 2021
%P 79-90
%V 1
%I mathdoc
%U http://geodesic.mathdoc.fr/item/BGUMI_2021_1_a6/
%G ru
%F BGUMI_2021_1_a6
R. E. Sharykin. Application of formal methods in the design of a single window system. Journal of the Belarusian State University. Mathematics and Informatics, Tome 1 (2021), pp. 79-90. http://geodesic.mathdoc.fr/item/BGUMI_2021_1_a6/

[1] M. N. Krasnyanskii, S. V. Karpushkin, A. V. Ostroukh, A. D. Obukhov, I. S. Kasatonov, D. V. Bukreev, “Proektirovanie informatsionnykh sistem upravleniya dokumentooborotom nauchno-obrazovatelnykh uchrezhdenii”, Izdatelstvo FGBOU VPO «TGTU», Tambov, 2015, 216

[2] R. E. Sharykin, A. N. Kurbatskii, “Verifikatsiya raspredelennykh ob'ektno orientirovannykh stokhasticheskikh gibridnykh sistem”, 9(3), Vesnik Grodzenskaga dzyarzhaunaga universiteta imya Yanki Kupaly. Matematyka. Fizika. Іnfarmatyka, vylichalnaya tekhnika i kiravanne, 2019, 123–132

[3] R. E. Sharykin, A. N. Kurbatskii, “Model raspredelennykh ob'ektno orientirovannykh stokhasticheskikh gibridnykh sistem”, Zhurnal Belorusskogo gosudarstvennogo universiteta. Matematika. Informatika, 2 (2019), 52–61 | MR | Zbl

[4] M. Clavel, F. Duran, S. Eker, P. Lincoln, N. Mart?-Oliet, J. Meseguer, “Maude: specification and programming in rewriting logic”, Theoretical Computer Science, 285(2) (2002), 187–243 | DOI | MR | Zbl

[5] R. E. Sharykin, SHYMaude specification of a single window document circulation system, Internet, GitHub Inc: {https://github.com/shymaude/singleWindow}, 2021

[6] K. Sen, M. Viswanathan, G. Agha, “On statistical model checking of stochastic systems. Computer aided verification”, Proceedings of the 17th International conference (Edinburgh, Scotland, UK), 3576, Springer-Verlag, Berlin, 2005, 266–280 | DOI | MR

[7] A. Vandin, S. Sebastio, “MultiVeStA: statistical model checking for discrete event simulators”, Proceedings of the 7th International conference on performance evaluation methodologies and tools procinfo Torino, Italy, Institute for Computer Sciences, Social Informatics and Telecommunications Engineering, Brussels, 2013, 310–315 | DOI

[8] G. Agha, J. Meseguer, K. Sen, “PMaude: rewrite-based specification language for probabilistic object systems”, Electronic Notes in Theoretical Computer Science, 153(2) (2006), 213–239 | DOI