Санкт-Петербург: СПбГУ ИТМО, 2011. - 246 с. В учебном пособии
рассматриваются вопросы верификации программного обеспечения на
основе проверки моделей с использованием различных языков
спецификации. Особое внимание уделяется верификации автоматных
программ, которые моделируются в виде системы автоматизированных
объектов управления и могут быть весьма эффективно верифицированы
указанным методом. Математический аппарат и прикладные инструменты
данной области позволяют создавать качественное программное
обеспечение для ответственных систем и получать надежные
подтверждения их правильности. Учебное пособие посвящено
концепциям, алгоритмам и инструментам для проверки моделей
программ. В нем излагаются теоретические вопросы проверки моделей,
вводятся различные спецификационные формализмы и описываются
алгоритмы проверки моделей для спецификаций, выраженных в этих
формализмах. Алгоритмы проверки моделей демонстрируются на примерах
конкретных инструментальных средств. Материал учебного пособия
предназначен для специалистов в области программирования,
информатики, вычислительной техники и систем управления, а также
студентов и аспирантов, обучающихся по специальностям «Прикладная
математика и информатика», «Управление и информатика в технических
системах» и «Вычислительные машины, системы, комплексы и сети».
Предполагается знакомство читателя с основными понятиями
математической логики, дискретной математики, теории графов и
теории алгоритмов.