К о з л о в
ПОДХОД К ВЕРИФИКАЦИИ МОДЕЛЕЙ СИСТЕМ
РЕАЛЬНОГО ВРЕМЕНИ С ПОМОЩЬЮ МЕТОДА
MODEL CHECKING
Рассмотрена задача построения алгоритма верификации систем
реального времени. <...> Предложен подход к проверке таких систем на
основе метода Model Checking. <...> Описаны основные шаги верификации, области применения разработанного подхода и приведены
примеры проверки различных моделей. <...> E-mail: arkandreev@gmail.com
Ключевые слова: система реального времени, проверка модели, временной автомат. <...> Основным способом решения этой проблемы является
верификация программ [1]. <...> Динамический подход подразумевает проверку программы в процессе исполнения и используется при тестировании программ. <...> Это можно сделать с помощью формальной
верификации. <...> Формальная верификация позволяет доказать соответствие программы своей спецификации. <...> При этом под спецификацией программы понимаются формализованные требования к ее поведению. <...> Одним
из основных направлений в рамках этого подхода является верификация модели программы (model checking) [2]. <...> Верификация модели программы требует решения ряда задач: необходимо построить по программе ее модель с конечным числом состояний и формально описать требования к программе в терминах
одного из видов темпоральных логик [3, 4]. <...> В результате верификации
модели либо подтверждается соответствие модели формализованным
требованиям, либо строится контрпример. <...> В последнем случае нужно определить причину некорректности: либо ошибка присутствует в
исходной программе, либо она появилась в результате некорректного
построения модели. <...> Также часто требуется решить задачу переноса
контрпримера в исходную программу. <...> Системы реального времени имеют особенности, которые делают
невозможной их проверку с помощью верификаторов общего назначения: при создании таких систем учитываются ограничения на временные характеристики функционирования, а значит, и верификатор
ISSN 0236-3933. <...> 2012
47
должен позволять проверять соответствие системы <...>