Применение формальных методов при проектировании системы одного окна

Предлагается подход, демонстрирующий разработку систем документооборота по принципу одного окна на раннем этапе их проектирования, основанный на применении формальных методов в части спецификации системы и метрик ее анализа, а также оценки значений метрик. Пример системы одного окна моделируется формально в рамках модели распределенных объектно ориентированных стохастических гибридных систем (РООСГС) с помощью языка спецификации SHYMaude. Предлагаются несколько метрик, позволяющих оценить систему. Данные метрики специфицируются формально посредством языка QuaTEx. Система одного окна, представленная как спецификация переписывающей логики Maude, полученная трансляцией спецификации SHYMaude, анализируется статистически с помощью инструмента MultiVeStA. В процессе статистического анализа определяется количество сотрудников, необходимое для эффективного функционирования системы. Полученное значение используется как стартовое значение в расширенной системе, в которой присутствует управление количеством сотрудников в целях поддержания длины очереди пакетов документов в желаемом диапазоне. При статистическом исследовании расширенной системы обнаруживается недостаток, который устраняется доработкой системы, что показывает, как данный подход может быть использован для изучения и доработки систем подобного типа на раннем этапе построения самой модели системы.