Редактирование: ВПнМ, список вопросов

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

Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.

Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.

= Список экзаменационных вопросов (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. Основные типы данных. Область видимости данных.

Пожалуйста, обратите внимание, что все ваши добавления могут быть отредактированы или удалены другими участниками. Если вы не хотите, чтобы кто-либо изменял ваши тексты, не помещайте их сюда.
Вы также подтверждаете, что являетесь автором вносимых дополнений, или скопировали их из источника, допускающего свободное распространение и изменение своего содержимого (см. eSyr's_wiki:Авторское право).
НЕ РАЗМЕЩАЙТЕ БЕЗ РАЗРЕШЕНИЯ ОХРАНЯЕМЫЕ АВТОРСКИМ ПРАВОМ МАТЕРИАЛЫ!

Описание изменений:

Отменить | Справка по редактированию (в новом окне)

Шаблоны, использованные на этой странице:

Шаблон:Курс ВПнМ

Получено с http://esyr.me/wiki/%D0%92%D0%9F%D0%BD%D0%9C%2C_%D1%81%D0%BF%D0%B8%D1%81%D0%BE%D0%BA_%D0%B2%D0%BE%D0%BF%D1%80%D0%BE%D1%81%D0%BE%D0%B2

Текущая версия		Ваш текст
Строка 1:		Строка 1:
-	''Взято с [https://docs.google.com/View?docid=dhf679dj_10dhnfpv28]''
-
	= Список экзаменационных вопросов (2008) =		= Список экзаменационных вопросов (2008) =

Редактирование: ВПнМ, список вопросов

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

Просмотры

Личные инструменты

Навигация

инструменты

Разделы

Спецкурсы

9 семестр

7 семестр

5 семестр

3 семестр

Поиск

Инструменты