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

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла

"Верификация программ на моделях"Список экзаменационных вопросов (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..

Характеристики

Тип файла PDF

PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

Список файлов вопросов/заданий