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