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/