Читать онлайн «Верификация автоматных программ: Учебное пособие»

МИНИСТЕРСТВО ОБРАЗОВАНИЯ И НАУКИ РОССИЙСКОЙ ФЕДЕРАЦИИ САНКТ-ПЕТЕРБУРГСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ ИНФОРМАЦИОННЫХ ТЕХНОЛОГИЙ, МЕХАНИКИ И ОПТИКИ С. Э. Вельдер, М. А. Лукин, А. А. Шалыто, Б. Р. Яминов ВЕРИФИКАЦИЯ АВТОМАТНЫХ ПРОГРАММ Учебное пособие Санкт-Петербург 2011 Рецензенты: Мелехин В. Ф. , докт. техн. наук, профессор, заведующий кафедрой компьютерных систем и программных технологий Санкт-Петербургского государственного политехнического университета Сергеев М. Б. , докт. техн. наук, профессор, заведующий кафедрой вычислительных систем и сетей Санкт-Петербургского государственного университета аэрокосмического приборостроения УДК 004. 42 Вельдер С. Э. , Лукин М. А. , Шалыто А. А. , Яминов Б. Р. Верификация автоматных программ. СПбГУ ИТМО, 2011. – 242 с. В учебном пособии рассматриваются вопросы верификации программного обеспечения на основе проверки моделей с использованием различных языков спецификации. Особое внимание уделяется верификации автоматных программ, которые моделируются в виде системы автоматизированных объектов управления и могут быть весьма эффективно верифицированы указанным методом. Математический аппарат и прикладные инструменты данной области позволяют создавать качественное программное обеспечение для ответственных систем и получать надежные подтверждения их правильности. Учебное пособие посвящено концепциям, алгоритмам и инструментам для проверки моделей программ. В нем излагаются теоретические вопросы проверки моделей, вводятся различные спецификационные формализмы и описываются алгоритмы проверки моделей для спецификаций, выраженных в этих формализмах. Алгоритмы проверки моделей демонстрируются на примерах конкретных инструментальных средств. Материал учебного пособия предназначен для специалистов в области программирования, информатики, вычислительной техники и систем управления, а также студентов и аспирантов, обучающихся по специальностям «Прикладная математика и информатика», «Управление и информатика в технических системах» и «Вычислительные машины, системы, комплексы и сети». Предполагается знакомство читателя с основными понятиями математической логики, дискретной математики, теории графов и теории алгоритмов. Рекомендовано к печати Ученым Советом университета В 2009 году Университет стал победителем многоэтапного конкурса, в результате которого определены 12 ведущих университетов России, которым присвоена категория «Национальный исследовательский университет». Министерством образования и науки Российской Федерации была утверждена Программа развития государственного образовательного учреждения высшего профессионального образования «Санкт- Петербургский государственный университет информационных технологий, механики и оптики» на 2009–2018 годы.  Санкт-Петербургский государственный университет информационных технологий, механики и оптики, 2011  Вельдер С.