2016 Экзаменационные задачи (1185505)
Текст из файла
Математические методы верификации схем и программ
Оглавление
Математические методы верификации схем и программ 1
Вариант 1 2
Задача 1 2
Задача 2 3
Задача 3 4
Задача 4 5
Задача 5 6
Задача 6 7
Задача 7 8
Задача 8 9
Задача 9 10
Задача 10 11
Вариант 2 12
Задача 1 12
Задача 2 13
Задача 3 14
Задача 4 15
Задача 5 16
Задача 6 17
Задача 7 18
Задача 8 19
Задача 9 20
Задача 10 21
Вариант 1
Задача 1
Докажите частичную корректность программы
относительно предусловия 
и постусловия .
Задача 2
Запишите формулу PLTL, которая адекватно соответствует следующему утверждению: «Верно хотя бы одно из двух: либо событие 
происходит почти всегда, либо сразу после каждого события 
два раза подряд случается событие ».
Задача 3
Определите, в каких состояниях модели 
выполнима формула 
Задача 4
Выбрав подходящий порядок переменных, построить ROBDD наименьшего размера для булевой функции
Задача 5
Определите, какие пары состояний модели являются бисимуляционно эквивалентными.
Задача 6
Какая формула называется инвариантом цикла?
Задача 7
Какое условие, налагаемое на пути в моделях программ, называется ограничением сильной справедливости? Зачем возникает необходимость в использовании ограничений справедливости?
Задача 8
Что называется неподвижной точкой преобразователя предикатов на множестве состояний модели программ? Докажите, что предикат 
является неподвижной точкой преобразователя предикатов 
.
Задача 9
Какое отношение между моделями Крипке называется отношением бисимуляции? Верно ли, что если две модели Крипке бисимуляционно эквивалентны, то на этих моделях выполняются одни и те же формулы логики CTL*?
Задача 10
Приведите определение понятия «временный автомат». Какое вычисление временного автомата называется вычислением Зенона?
Вариант 2
Задача 1
Докажите частичную корректность программы
относительно предусловия и постусловия .
Задача 2
Запишите формулу PLTL, которая адекватно соответствует следующему утверждению: «Верно, что если событие происходит почти всегда, то после трёх будет ».
Задача 3
Определите, в каких состояниях модели выполнима формула 
Задача 4
Выбрав подходящий порядок переменных, построить ROBDD наименьшего размера для булевой функции
Задача 5
Определите, какие пары состояний модели являются бисимуляционно эквивалентными.
Задача 6
Какое предусловие ψ называется слабейшим для функции π и условия φ.
Задача 7
Определение свойства живучести. Пример двух свойств системы, где одно – свойство живучести, а другое нет.
Задача 8
Обобщённый автомат Бюхи и какие слова он распознаёт?
Задача 9
Конус влияния и зачем он нужен?
Задача 10
Определение задачи BMC. Коэффициент сложности.
Характеристики
Тип файла документ
Документы такого типа открываются такими программами, как Microsoft Office Word на компьютерах Windows, Apple Pages на компьютерах Mac, Open Office - бесплатная альтернатива на различных платформах, в том числе Linux. Наиболее простым и современным решением будут Google документы, так как открываются онлайн без скачивания прямо в браузере на любой платформе. Существуют российские качественные аналоги, например от Яндекса.
Будьте внимательны на мобильных устройствах, так как там используются упрощённый функционал даже в официальном приложении от Microsoft, поэтому для просмотра скачивайте PDF-версию. А если нужно редактировать файл, то используйте оригинальный файл.
Файлы такого типа обычно разбиты на страницы, а текст может быть форматированным (жирный, курсив, выбор шрифта, таблицы и т.п.), а также в него можно добавлять изображения. Формат идеально подходит для рефератов, докладов и РПЗ курсовых проектов, которые необходимо распечатать. Кстати перед печатью также сохраняйте файл в PDF, так как принтер может начудить со шрифтами.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
