ВПнМ, список вопросов
Материал из eSyr's wiki.
Содержание |
Список экзаменационных вопросов (2008)
Моделирование и абстракция
- Моделирование программ. Понятие состояния. Потенциальные и достижимые состояния. Требования к модели. Процесс построения модели.
- Моделирование программ. Размеченные системы переходов. Детерминизм и недетерминизм. Вычисления и трассы. Свойства линейного времени. Выполнимость свойства на трассе.
- Моделирование программ. Графы программ. Статическая и операционная семантика.
- Параллелизм. Чередование систем переходов.
- Параллелизм. Чередование графов программ. Случаи без разделяемых переменных и с разделяемыми переменными.
- Параллелизм. Синхронный параллелизм. Рандеву.
- Параллелизм. Асинхронный параллелизм. Системы с каналами. Операционная семантика.
- Абстракция. Абстракция трасс. Абстракция системы переходов. Необходимое и достаточное условие корректности LTS модели.
- Абстракция. Абстракция системы переходов. Достаточное условие корректности LTS модели. Адекватность LTS модели.
- Абстракция. Абстракция графов программ. Отношение слабой симуляции.
Логика LTL, автоматы Бюхи
- Свойства правильности. Формулирование требований правильности программы. Двойственность. Типы свойств.
- Свойства правильности. Свойства безопасности и живучести. Проверка таких свойств. Примеры свойств.
- Автоматы Бюхи. Конечные автоматы. Проход автомата. Язык автомата.
- Автоматы Бюхи. Омега-допускание. Расширение автоматов Бюхи.
- Логика LTL. Синтаксис LTL. Семантика выполнимости формул. Сильный и слабый until.
- Логика LTL. Основные типы свойств LTL. Цикличность, стабильность, инвариант, гарантия, отклик, приоритет, корреляция.
- Логика LTL. Эквивалентные преобразования формул LTL.
- Логика LTL. Оператор neXt. Свойства, инвариантные к прореживанию.
- Логика LTL. Проверка выполнимости формул LTL при помощи автоматов Бюхи. Проверка LTL-формул в Spin.
- Логика LTL. Выразительная мощность LTL. Логики LTL + существование, CTL* и CTL. Сравнение выразительной мощности.
Верификация программ на моделях
- Задача проверки правильности программ. Валидация. Верификация. Системы с повышенными требованиями к надёжности. Реактивные программы. Параллельные программы. Особенности верификации таких программ.
- Подходы к верификации программ. Тестирование и имитационное моделирование. Область применения, плюсы и минусы. Проблема полноты тестового покрытия.
- Подходы к верификации программ. Доказательство теорем. Область применения, плюсы и минусы.
- Подходы к верификации программ. Статический анализ исходного кода программ. Область применения, плюсы и минусы.
- Подходы к верификации программ. Верификация программ на моделях. Процесс верификации программы при помощи её модели. Область применения, плюсы и минусы.
- Верификация на моделях. История развития верификации программ на моделях. Схема верификации программ на моделях. Классы проверяемых свойств правильности программы.
- Верификация при помощи Spin. Задание свойств состояний.
- Верификация при помощи Spin. Задание свойств последовательностей состояний. Циклы бездействия. Ограничения справедливости.
- Верификация при помощи Spin. Задание свойств последовательностей состояний. Утверждения о невозможности. Трассовые ассерты.
- Верификация при помощи Spin. Принцип верификации нарушения свойств. Контрпримеры. Процесс верификации при помощи Spin. Использование LTL в Spin.
Система Spin и язык Promela
- Система Spin. Процесс моделирования и верификации при помощи системы Spin. Конечность моделей на Promela. Асинхронное выполнение моделей. Недетерминированный поток управления. Понятие выполнимости оператора.
- Язык Promela. Основные компоненты модели на языке Promela. Процессы, локальные и глобальные объекты данных, каналы сообщений.
- Язык Promela. Механизмы взаимодействия процессов в языке Promela. Глобальные переменные, каналы сообщений, явная синхронизация.
- Язык Promela. Основные операторы языка Promela. Операторы-выражения, присваивания.
- Язык Promela. Основные операторы языка Promela. Отладочная печать, операторы skip, true, run, assert.
- Язык Promela. Чередование (интерливинг) операторов. Внешний и внутренний недетерминизм. Управление выполнимостью операторов.
- Язык Promela. Задание потока управления последовательного процесса. Управляющие конструкции if, do. Организация внутреннего недетерминизма.
- Язык Promela. Каналы сообщений. Операторы отправки и приёма сообщений. Тип mtype. синхронная и асинхронная передача сообщений.
- Язык Promela. Каналы сообщений. Вспомогательные операции с каналами сообщений.
- Язык Promela. Основные типы данных. Область видимости данных.
