Верификация автоматных програм

Вельдер С.Э., Лукин М.А., Шалыто А.А., Яминов Б.Р. — Санкт-Петербург: Наука, 2011. — 244 с. — ISBN 978-5-02-038160-5.В книге рассматриваются вопросы верификации программного обеспечения на основе проверки моделей с использованием различных языков спецификации. Особое внимание уделяется верификации автоматных программ, которые моделируются в виде системы автоматизированных объектов управления и могут быть весьма эффективно верифицированы указанным методом. Математический аппарат и прикладные инструменты данной области позволяют создавать качественное программное обеспечение для ответственных систем и получать надежные подтверждения их правильности. Книга посвящена концепциям, алгоритмам и инструментам для проверки моделей программ. В ней излагаются теоретические вопросы проверки моделей, вводятся различные спецификационные формализмы и описываются алгоритмы проверки моделей для спецификаций, выраженных в этих формализмах. Алгоритмы проверки моделей демонстрируются на примерах конкретных инструментальных средств. Данная книга предназначена для специалистов в области программирования, информатики, вычислительной техники и систем управления, а также студентов и аспирантов, обучающихся по специальностям «Прикладная математика и информатика», «Управление и информатика в технических системах» и «Вычислительные машины, системы, комплексы и сети». Предполагается знакомство читателя с основными понятиями математической логики, дискретной математики, теории графов и теории алгоритмов. Книга может быть использована в качестве учебного пособия.ВведениеВалидация системЗадачи валидации системСимуляцияТестированиеФормальная верификацияПроверка моделейАвтоматическое доказательство теоремМатематический аппарат верификации моделейМоделирование системыПроверка моделей для линейной темпоральной логикиСинтаксис LTLСемантика LTLАксиоматизацияРасширения LTLСпецификация свойств в LTLПроверка моделей для LTLВерификация LTL при помощи автоматов БюхиПроверка моделей для ветвящейся темпоральной логикиСинтаксис CTLСемантика CTLНекоторые аксиомы CTLСравнение выразительной силы CTL, CTL* и LTLСпецификация свойств в CTLУсловия справедливости в CTLПроверка моделей для CTL и CTL*Поиск справедливых путейДвойной обход в глубинуПоиск сильно связных компонентПроверка моделей для темпоральной логики реального времениВременные автоматыСемантика временных автоматовСинтаксис TCTLСемантика TCTLСпецификация временных свойств в TCTLЭквивалентность часовых оценокРегионные автоматыПроверка моделей для регионных автоматовСети ПетриОбзор верификаторовSPINSMVВерификация автоматных программАвтоматные программыОбзор существующих решенийСредства и объекты верификацииМодель банкоматаВерифицируемые свойства банкоматаИнструменты, использующие готовые верификаторыConverterUnimod.VerifierFSM VerifierАвтономные верификаторыCTL VerifierAutomata VerificatorЗаключениеСписок источниковАлфавитный указатель