4. NuSMV - обзор средства., страница 2
Описание файла
PDF-файл из архива "4. NuSMV - обзор средства.", который расположен в категории "". Всё это находится в предмете "математические методы верификации схем и программ" из 11 семестр (3 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 2 страницы из PDF
. . , xn ), описаннымили порождённым в модуле, экземпляр e которогообъявлен в модуле m, порождается ограничение JUSTICEϕ {x1 /e.x1 , . . . xn /e.xn } в модуле m(ν) СправедливостьВ данном примере модель M[main] совпадает с модельюпредыдущего примера, и в модуле main порождаются дваограничения справедливости:IJUSTICE turn = 1;IJUSTICE turn = 2;Содержательная трактовка этих ограничений справедливости:несправедливый путь — это путь,в котором какой-либо из процессов в некоторый моментнавсегда становится неактивным(ν) Нетотальные модели КрипкеСогласно определению в лекции 3, модель Крипке — этототальный граф: из каждой вершины исходит хотя бы однадугаВо многих средствах верификации (в том числе NuSMV ) можноописывать такие модели, граф которых нетоталенТакие модели (нетотальные модели Крипке) обычно считаютсянекорректными, за исключением случаев, явно описанных вдокументацииВ частности, при “наивном” использовании NuSMV для проверкиCTL-формул нетотальные модели крипке всегда некорректны:результат верификации не отражает в полной мере устройствомоделиСледить за тотальностью модели — этозадача того, кто описывает модель(ν) Нетотальные модели Крипке···Конец семинара 4.