Logo BSU

Please use this identifier to cite or link to this item: https://elib.bsu.by/handle/123456789/258441
Title: Применение формальных методов при проектировании системы одного окна
Other Titles: Application of formal methods in the design of a single window system / R. E. Sharykin
Authors: Шарыкин, Р. Е.
Keywords: ЭБ БГУ::ОБЩЕСТВЕННЫЕ НАУКИ::Информатика
Issue Date: 2021
Publisher: Минск : БГУ
Citation: Журнал Белорусского государственного университета. Математика. Информатика = Journal of the Belarusian State University. Mathematics and Informatics. - 2021. - № 1. - С. 79-90
Abstract: Предлагается подход, демонстрирующий разработку систем документооборота по принципу одного окна на раннем этапе их проектирования, основанный на применении формальных методов в части спецификации системы и метрик ее анализа, а также оценки значений метрик. Пример системы одного окна моделируется формально в рамках модели распределенных объектно ориентированных стохастических гибридных систем (РООСГС) с помощью языка спецификации SHYMaude. Предлагаются несколько метрик, позволяющих оценить систему. Данные метрики специфицируются формально посредством языка QuaTEx. Система одного окна, представленная как спецификация переписывающей логики Maude, полученная трансляцией спецификации SHYMaude, анализируется статистически с помощью инструмента MultiVeStA. В процессе статистического анализа определяется количество сотрудников, необходимое для эффективного функционирования системы. Полученное значение используется как стартовое значение в расширенной системе, в которой присутствует управление количеством сотрудников в целях поддержания длины очереди пакетов документов в желаемом диапазоне. При статистическом исследовании расширенной системы обнаруживается недостаток, который устраняется доработкой системы, что показывает, как данный подход может быть использован для изучения и доработки систем подобного типа на раннем этапе построения самой модели системы.
Abstract (in another language): 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.
URI: https://elib.bsu.by/handle/123456789/258441
ISSN: 1561-834X
DOI: 10.33581/2520-6508-2021-1-79-90
Licence: info:eu-repo/semantics/openAccess
Appears in Collections:2021, №1

Files in This Item:
File Description SizeFormat 
79-90.pdf1,89 MBAdobe PDFView/Open
Show full item record Google Scholar



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.