Стр. 14 - А.М. Андреев, И.А. Козлов - Подход к верификации моделей систем реального времени с помощью метода Model Checking
Упрощенная HTML-версия
К недостаткам подхода можно отнести сложность его примене-
ния для больших программных систем. Даже верификаторы общего
назначения зачастую плохо справляются с проблемой комбинаторно-
го взрыва в пространстве состояний, возникающего с ростом размера
входной модели. Для систем реального времени эта проблема стоит
особенно остро, ведь помимо выделения локаций, выполняемого в
любом верификаторе, нужно провести разбиение этих локаций на от-
дельные временн ´ые зоны. Этот этап усугубляет проблему роста числа
состояний, а также значительно увеличивает время выполнения вери-
фикации. Описанный в статье подход позволяет отчасти решить пер-
вую из этих проблем: итоговое число состояний значительно меньше,
чем может быть получено другими методами (такими, как построение
графа регионов).
СПИСОК ЛИТЕРАТУРЫ
1. К у з ь м и н Е. В., С о к о л о в В. А. О дисциплине специализации “Верифи-
кация программ” // Докл. II науч.-методич. конф. “Преподавание математики в
компьютерных науках”, Ярославль: ЯрГУ. 2007.
2. К л а р к Э. М., Г р а м б е р г О., П е л е д Д. Верификация моделей программ:
Model checking. – М.: МНЦМО, 2002.
3. P n u e l i A. The temporal logic of programs // Proceedings of the 18th IEEE
Symposium on Foundation of Computer Science. 1977.
4. E m e r s o n E. A. Temporal and modal logic // Handbook of Theoretical Computer
Science. Chapter 16. 1990.
5. В е л ь д е р С. Э., Л у к и н М. А., Ш а л ы т о А. А., Я м и н о в Б. Р.
Верификация автоматных программ. – СПб.: ГУ ИТМО, 2011. – 240 с.
6. Ш а л ы т о А. А. Программная реализация управляющих автоматов // Судо-
строительная промышленность. Сер. Автоматика и телемеханика. – 1991. –
Вып. 13.
7. Ш а л ы т о А. А. SWITCH-технология. Алгоритмизация и программирование
задач логического управления. – СПб.: Наука. 1998.
8. К а р п о в Ю. Г. MODEL CHECKING. Верификация параллельных и распре-
деленных программных систем. – СПб.: БХВ-Петербург, 2010.
Статья поступила в редакцию 15.12.2011
60
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012
