СПб: СПбГУ ИТМО, 2011. – 242 с.
В учебном пособии рассматриваются вопросы верификации программного
обеспечения на основе проверки моделей с использованием различных
языков
спецификации. Особое внимание уделяется верификации автоматных программ, которые моделируются в виде системы автоматизированных объектов управления и могут быть весьма эффективно верифицированы указанным методом. Математический аппарат и прикладные инструменты данной области позволяют создавать качественное программное обеспечение для ответственных систем и получать надежные подтверждения их правильности. Учебное пособие посвящено концепциям, алгоритмам и инструментам для проверки моделей программ. В нем излагаются теоретические вопросы проверки моделей, вводятся различные спецификационные формализмы и описываются алгоритмы проверки моделей для спецификаций, выраженных в этих формализмах. Алгоритмы проверки моделей
демонстрируются на примерах конкретных инструментальных средств. Материал учебного пособия предназначен для специалистов в области программирования, информатики, вычислительной техники и систем управления, а также студентов и аспирантов, обучающихся по специальностям «Прикладная математика и информатика», «Управление и информатика в технических системах» и «Вычислительные машины, системы, комплексы и сети». Предполагается знакомство читателя с основными понятиями математической
логики, дискретной математики, теории графов и теории алгоритмов.
Содержание
Введение
Валидация систем
Задачи валидации систем
Симуляция
Тестирование
Формальная верификация
Проверка моделей
Автоматическое доказательство теорем
Математический аппарат верификации моделей
Моделирование системы
Проверка моделей для линейной темпоральной логики
Синтаксис LTL
Семантика LTL
Аксиоматизация
Расширения LTL
Спецификация свойств в LTL
Проверка моделей для LTL
Верификация LTL при помощи автоматов Бюхи
Проверка моделей для ветвящейся темпоральной логики
Синтаксис CTL
Семантика CTL
Некоторые аксиомы CTL
Сравнение выразительной силы CTL, CTL* и LTL
Спецификация свойств в CTL
Условия справедливости в CTL
Проверка моделей для CTL и CTL*
Поиск справедливых путей
Двойной обход в глубину
Поиск сильно связных компонент
Проверка моделей для темпоральной логики реального времени
Временные автоматы
Семантика временных автоматов
Синтаксис TCTL
Семантика TCTL
Спецификация временных свойств в TCTL
Эквивалентность часовых оценок
Регионные автоматы
Проверка моделей для регионных автоматов
Сети Петри
Обзор верификаторов
SPIN
SMV
Верификация автоматных программ
Автоматные программы
Обзор существующих решений
Средства и объекты верификации
Модель банкомата
Верифицируемые свойства банкомата
Инструменты, использующие готовые верификаторы
Converter
Unimod.Verifier
FSM Verifier
Автономные верификаторы
CTL Verifier
Automata Verificator
Заключение
Список источников
Алфавитный указатель
спецификации. Особое внимание уделяется верификации автоматных программ, которые моделируются в виде системы автоматизированных объектов управления и могут быть весьма эффективно верифицированы указанным методом. Математический аппарат и прикладные инструменты данной области позволяют создавать качественное программное обеспечение для ответственных систем и получать надежные подтверждения их правильности. Учебное пособие посвящено концепциям, алгоритмам и инструментам для проверки моделей программ. В нем излагаются теоретические вопросы проверки моделей, вводятся различные спецификационные формализмы и описываются алгоритмы проверки моделей для спецификаций, выраженных в этих формализмах. Алгоритмы проверки моделей
демонстрируются на примерах конкретных инструментальных средств. Материал учебного пособия предназначен для специалистов в области программирования, информатики, вычислительной техники и систем управления, а также студентов и аспирантов, обучающихся по специальностям «Прикладная математика и информатика», «Управление и информатика в технических системах» и «Вычислительные машины, системы, комплексы и сети». Предполагается знакомство читателя с основными понятиями математической
логики, дискретной математики, теории графов и теории алгоритмов.
Содержание
Введение
Валидация систем
Задачи валидации систем
Симуляция
Тестирование
Формальная верификация
Проверка моделей
Автоматическое доказательство теорем
Математический аппарат верификации моделей
Моделирование системы
Проверка моделей для линейной темпоральной логики
Синтаксис LTL
Семантика LTL
Аксиоматизация
Расширения LTL
Спецификация свойств в LTL
Проверка моделей для LTL
Верификация LTL при помощи автоматов Бюхи
Проверка моделей для ветвящейся темпоральной логики
Синтаксис CTL
Семантика CTL
Некоторые аксиомы CTL
Сравнение выразительной силы CTL, CTL* и LTL
Спецификация свойств в CTL
Условия справедливости в CTL
Проверка моделей для CTL и CTL*
Поиск справедливых путей
Двойной обход в глубину
Поиск сильно связных компонент
Проверка моделей для темпоральной логики реального времени
Временные автоматы
Семантика временных автоматов
Синтаксис TCTL
Семантика TCTL
Спецификация временных свойств в TCTL
Эквивалентность часовых оценок
Регионные автоматы
Проверка моделей для регионных автоматов
Сети Петри
Обзор верификаторов
SPIN
SMV
Верификация автоматных программ
Автоматные программы
Обзор существующих решений
Средства и объекты верификации
Модель банкомата
Верифицируемые свойства банкомата
Инструменты, использующие готовые верификаторы
Converter
Unimod.Verifier
FSM Verifier
Автономные верификаторы
CTL Verifier
Automata Verificator
Заключение
Список источников
Алфавитный указатель