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