Стр. 13 - А.М. Андреев, И.А. Козлов - Подход к верификации моделей систем реального времени с помощью метода Model Checking

Рис. 9. Граф переходов автомата A1
Рис. 10. Граф переходов автомата A2
При анализе результатов верификации становится понятна причи-
на такого результата: при выборе спецификации не было учтено, что
автомат A2 может находиться в состоянии s21 сколь угодно долго.
Заключение. Предложен подход к верификации систем реально-
го времени на основе метода Model Checking. Данный подход может
применяться для выявления ошибок в программах на этапе детализи-
рованного проектирования систем реального времени. В соответствии
с описанным подходом была разработана система верификации, отли-
чающаяся от существующих средств своей универсальностью. С ее
помощью можно проверять временн ´ые автоматы (модели, используе-
мые для описания поведения асинхронных систем реального времени),
автоматные программы, а также множество других моделей, исполь-
зуемых в различных классах программных систем.
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012 59