Метод формализации описания поведения систем управления в ходе проектирования программного обеспечения

Рассмотрен метод формализации исходных данных, описывающих поведение систем управления (СУ), путем получения структуры Крипке и набора темпоральных формул на основе набора прецедентов работы системы. Процесс формализации рассмотрен на примере описания работы автоматизированного анализатора уровня активности холинэстераз плазмы и эритроцитов крови человека "Гранат-4". Полученное описание может служить основой как для реализации программного обеспечения СУ, так и для анализа и исследования особенностей работы СУ с помощью методов Model checking, формальных методов верификации или средств построения и контроля сценариев проверки.