Подход к верификации моделей систем реального времени с помощью метода Model Checking
Опубликовано: 31.12.2012
Авторы: Андреев А.М., Козлов И.А.
Опубликовано в выпуске: #11(11)/2012
DOI: 10.18698/2308-6033-2012-11-478
Раздел: Информационные технологии | Рубрика: Компьютерные системы и сети
Рассмотрена задача построения алгоритма верификации систем реального времени. Предложен подход к проверке таких систем на основе метода Model Checking. Описаны основные шаги верификации, области применения разработанного подхода и приведены примеры проверки различных моделей.
Литература
[1] Кузьмин Е.В., Соколов В.А. О дисциплине специализации “Верификация программ” // Докл. II науч.-методич. конф. “Преподавание математики в компьютерных науках”, Ярославль: ЯрГУ. 2007
[2] Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: Model checking. – М.: МНЦМО, 2002
[3] Pnueli A. The temporal logic of programs // Proceedings of the 18th IEEE Symposium on Foundation of Computer Science. 1977
[4] Emerson 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