Список экзаменационных вопросов
Описание файла
PDF-файл из архива "Список экзаменационных вопросов", который расположен в категории "". Всё это находится в предмете "верификация программ на моделях" из 8 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст из PDF
"Верификация программ на моделях"Список экзаменационных вопросов (2009)Моделирование и абстракцияМоделирование программ. Понятие состояния. Потенциальные идостижимые состояния. Требования к модели. Процесс построения модели.2.Моделирование программ. Размеченные системы переходов.Детерминизм и недетерминизм. Вычисления и трассы. Свойства линейноговремени.
Выполнимость свойства на трассе.3.Моделирование программ. Графы программ. Статическая иоперационная семантика.4.Параллелизм. Чередование систем переходов.5.Параллелизм. Чередование графов программ. Случаи без разделяемыхпеременных и с разделяемыми переменными.6.Параллелизм. Синхронный параллелизм. Рандеву.7.Параллелизм. Асинхронный параллелизм. Системы с каналами.Операционная семантика.8.Абстракция.
Абстракция трасс. Абстракция системы переходов.Необходимое и достаточное условие корректности LTS модели.9.Абстракция. Абстракция системы переходов. Достаточное условиекорректности LTS модели. Адекватность LTS модели.10.Абстракция. Абстракция графов программ. Отношение слабойсимуляции.1.Логика LTL, автоматы БюхиСвойства правильности. Формулирование требований правильностипрограммы. Двойственность. Типы свойств.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.1.Система Spin и язык PromelaСистема 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. Основные типы данных. Область видимости данных. 1..
