Семинар 5.2. NuSMV практика
Описание файла
PDF-файл из архива "Семинар 5.2. NuSMV практика", который расположен в категории "". Всё это находится в предмете "математические методы верификации схем и программ" из 10 семестр (2 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст из PDF
Математические методыверификации схем ипрограммЛекторы:Захаров Владимир АнатольевичПодымов Владислав Васильевичe-mail рассказчика:valdus@yandex.ruОсень 2016Семинар 5-6NuSMV: практикаintegerprocessДомашнее задание“Недотип” integerИз документации:Значения типа integer — это любые целые числа. <...> Наданный момент точная область определения зависит отмакроопределений C/C++: от INT_MIN + 1 до INT_MAX<тип > ::boolean| [unsigned | signed] word [<выражение >]| { <перечисление > }| <выражение >..<выражение >| array <выражение >..<выражение > of <тип >Как работает асинхронная композицияИз документации:Шаг [асинхронного] выполнения системы состоит вIнедетерминированном выборе процессаIодновременном (параллельном) выполнении всехинструкций видаASSIGN next(<переменная >) = ...Iсохранении значений всех переменных, невстретившихся в левой части выполнившихсяинструкцийIдобавлении к результату остальных ограничений: TRANS, ...Домашнее заданиеЗадание можно выполнять одному, можно вдвоёмНаписать мне на почту письмо с заголовком“[ver 2016 nusmv] Фамилия И.О.” или“[ver 2016 nusmv] Фамилия И.О.
Фамилия И.О.”и любым содержаниемВ ответ я пришлю описание системы и требований(как в последнем домашнем задании)Задача:1. описать систему и требования в формате NuSMV2. убедиться, что всё написано правильно (в числе прочего вNuSMV есть симуляция)3. прислать .smv-файл ответом на мой ответ на исходноеписьмоМожно в содержании письма излагать пожелания онаправленности задания(в задачах семинара будет несколько таких направленностей)Домашнее заданиеДля допуска к экзамену это домашнее задание должнобыть решеноВ худшем случае оно будет решаться непосредственно передэкзаменом за очень короткое время, так что лучше сделайтевсё сейчасРешение о том, принято ли задание, будет приниматьсяодин раз, если не считать попытки перед экзаменомПоэтому рекомендуется использовать все средствасамопроверки, а при работе в паре - взаимной проверкиКрайний срок сдачи:15 ноября, 23:59.