Материал из eSyr's wiki.

---

Версия 02:06, 26 февраля 2009

Содержание 1 Список экзаменационных вопросов (2008) 1.1 Моделирование и абстракция 1.2 Логика LTL, автоматы Бюхи 1.3 Верификация программ на моделях 1.4 Система Spin и язык Promela

Список экзаменационных вопросов (2008)

Моделирование и абстракция

1. Моделирование программ. Понятие состояния. Потенциальные и достижимые состояния. Требования к модели. Процесс построения модели.
2. Моделирование программ. Размеченные системы переходов. Детерминизм и недетерминизм. Вычисления и трассы. Свойства линейного времени. Выполнимость свойства на трассе.
3. Моделирование программ. Графы программ. Статическая и операционная семантика.
4. Параллелизм. Чередование систем переходов.
5. Параллелизм. Чередование графов программ. Случаи без разделяемых переменных и с разделяемыми переменными.
6. Параллелизм. Синхронный параллелизм. Рандеву.
7. Параллелизм. Асинхронный параллелизм. Системы с каналами. Операционная семантика.
8. Абстракция. Абстракция трасс. Абстракция системы переходов. Необходимое и достаточное условие корректности LTS модели.
9. Абстракция. Абстракция системы переходов. Достаточное условие корректности LTS модели. Адекватность LTS модели.
10. Абстракция. Абстракция графов программ. Отношение слабой симуляции.

Логика LTL, автоматы Бюхи

1. Свойства правильности. Формулирование требований правильности программы. Двойственность. Типы свойств.
2. Свойства правильности. Свойства безопасности и живучести. Проверка таких свойств. Примеры свойств.
3. Автоматы Бюхи. Конечные автоматы. Проход автомата. Язык автомата.
4. Автоматы Бюхи. Омега-допускание. Расширение автоматов Бюхи.
5. Логика LTL. Синтаксис LTL. Семантика выполнимости формул. Сильный и слабый until.
6. Логика LTL. Основные типы свойств LTL. Цикличность, стабильность, инвариант, гарантия, отклик, приоритет, корреляция.
7. Логика LTL. Эквивалентные преобразования формул LTL.
8. Логика LTL. Оператор neXt. Свойства, инвариантные к прореживанию.
9. Логика LTL. Проверка выполнимости формул LTL при помощи автоматов Бюхи. Проверка LTL-формул в Spin.
10. Логика LTL. Выразительная мощность LTL. Логики LTL + существование, CTL* и CTL. Сравнение выразительной мощности.

Верификация программ на моделях

1. Задача проверки правильности программ. Валидация. Верификация. Системы с повышенными требованиями к надёжности. Реактивные программы. Параллельные программы. Особенности верификации таких программ.
2. Подходы к верификации программ. Тестирование и имитационное моделирование. Область применения, плюсы и минусы. Проблема полноты тестового покрытия.
3. Подходы к верификации программ. Доказательство теорем. Область применения, плюсы и минусы.
4. Подходы к верификации программ. Статический анализ исходного кода программ. Область применения, плюсы и минусы.
5. Подходы к верификации программ. Верификация программ на моделях. Процесс верификации программы при помощи её модели. Область применения, плюсы и минусы.
6. Верификация на моделях. История развития верификации программ на моделях. Схема верификации программ на моделях. Классы проверяемых свойств правильности программы.
7. Верификация при помощи Spin. Задание свойств состояний.
8. Верификация при помощи Spin. Задание свойств последовательностей состояний. Циклы бездействия. Ограничения справедливости.
9. Верификация при помощи Spin. Задание свойств последовательностей состояний. Утверждения о невозможности. Трассовые ассерты.
10. Верификация при помощи Spin. Принцип верификации нарушения свойств. Контрпримеры. Процесс верификации при помощи Spin. Использование LTL в Spin.

Система Spin и язык Promela

1. Система Spin. Процесс моделирования и верификации при помощи системы Spin. Конечность моделей на Promela. Асинхронное выполнение моделей. Недетерминированный поток управления. Понятие выполнимости оператора.
2. Язык Promela. Основные компоненты модели на языке Promela. Процессы, локальные и глобальные объекты данных, каналы сообщений.
3. Язык Promela. Механизмы взаимодействия процессов в языке Promela. Глобальные переменные, каналы сообщений, явная синхронизация.
4. Язык Promela. Основные операторы языка Promela. Операторы-выражения, присваивания.
5. Язык Promela. Основные операторы языка Promela. Отладочная печать, операторы skip, true, run, assert.
6. Язык Promela. Чередование (интерливинг) операторов. Внешний и внутренний недетерминизм. Управление выполнимостью операторов.
7. Язык Promela. Задание потока управления последовательного процесса. Управляющие конструкции if, do. Организация внутреннего недетерминизма.
8. Язык Promela. Каналы сообщений. Операторы отправки и приёма сообщений. Тип mtype. синхронная и асинхронная передача сообщений.
9. Язык Promela. Каналы сообщений. Вспомогательные операции с каналами сообщений.
10. Язык Promela. Основные типы данных. Область видимости данных.