2016 Экзаменационные задачи (1185506)

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

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

Математические методы верификации схем и программОглавлениеМатематические методы верификации схем и программ ................................... 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Задача 2Запишите формулу PLTL, которая адекватно соответствует следующемуутверждению: «Верно хотя бы одно из двух: либо событие происходитпочти всегда, либо сразу после каждого события два раза подряд случаетсясобытие ».3Задача 3Определите, в каких( ) ( )12{}Ø4Øсостояниях5{}выполнима6{}3модели89{}Ø7{}{, }4формула10Ø12Ø11{}Задача 4Выбрав подходящий порядок переменных, построить ROBDD наименьшегоразмера для булевой функции(1 , 2 , 3 , 4 , 5 , 6 ) = (2 ⊕ 6 )˄(4 ≡ 3 )˄(1 ⊕ 5 )5Задача 5Определите, какие пары состояний модели являются бисимуляционноэквивалентными.1{, }2{}4{, }5{}3{}6{, }87{}{}69{}10{, }12{, }11{}Задача 6Какая формула называется инвариантом цикла?7Задача 7Какое условие, налагаемое на пути в моделях программ, называетсяограничением сильной справедливости? Зачем возникает необходимость виспользовании ограничений справедливости?8Задача 8Что называется неподвижной точкой преобразователя предикатов намножестве состояний модели программ? Докажите, что предикат является неподвижной точкой преобразователя предикатов () = ˄.9Задача 9Какое отношение между моделями Крипке называется отношениембисимуляции? Верно ли, что если две модели Крипке бисимуляционноэквивалентны, то на этих моделях выполняются одни и те же формулылогики CTL*?10Задача 10Приведите определение понятия «временный автомат».

Какое вычислениевременного автомата называется вычислением Зенона?11Вариант 2Задача 1Докажите частичную корректность программы < ≔ + ; ≔ − ; ≔ − < ≔ +1 ;относительно предусловия + = и постусловия + = .12Задача 2Запишите формулу PLTL, которая адекватно соответствует следующемуутверждению: «Верно, что если событие происходит почти всегда, то послетрёх будет ».13Задача 3Определите, в каких( ) ( )1{, }2{}4{, }состояниях5{}выполнима6{}3модели{, }87{}Ø14формула9{}10{, }12{, }11{}Задача 4Выбрав подходящий порядок переменных, построить ROBDD наименьшегоразмера для булевой функции(1 , 2 , 3 , 4 , 5 , 6 ) = (1 ⊕ 5 )˄(2 ≡ 3 )˄(4 ≡ 6 )15Задача 5Определите, какие пары состояний модели являются бисимуляционноэквивалентными.1{, }2{}4{, }5{}3{}6{, }87{}{, }169{}10{, }12{, }11{}Задача 6Какое предусловие ψ называется слабейшим для функции π и условия φ.17Задача 7Определение свойства живучести.

Пример двух свойств системы, где одно –свойство живучести, а другое нет.18Задача 8Обобщённый автомат Бюхи и какие слова он распознаёт?19Задача 9Конус влияния и зачем он нужен?20Задача 10Определение задачи BMC. Коэффициент сложности.21.

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

Тип файла PDF

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

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

Список файлов ответов (шпаргалок)