И.В. Шошмина, Ю.Г. Карпов - Введение в язык Promela и систему комплексной верификации Spin, страница 14
Описание файла
PDF-файл из архива "И.В. Шошмина, Ю.Г. Карпов - Введение в язык Promela и систему комплексной верификации Spin", который расположен в категории "". Всё это находится в предмете "верификация программ на моделях" из 8 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 14 страницы из PDF
Параметры верификации базовых свойствВыберете пункт Set Verification Parameters меню Run. Откроется диалоговое окно ВаsicVerification Options.На панели Correctness Properties указываются базовые свойства, которые можноверифицировать:•Safety – свойства безопасностиo Assertions – проверка сохранения локальных инвариантов, описанных припомощи оператора assert (см. 2.1);o Invalid Endstates – проверка на наличие некорректных конечных состояний, т.е.обнаружение взаимных блокировок процессов (см.
2.2);•Liveness – свойства живостиo Non-Progress Cycles – проверка отсутствия бесконечных циклов,содержащих операторов, помеченных меткой progress (см. 2.3);неo Acceptance Cycles – проверка отсутствия циклов, с бесконечно частымвыполением операторов с меткой accept (см. 2.4).•Apply Never Claim – учитывать процесс never, если таковой имеется в тексте модели(см.
2.5).•Report Unreachable Code – выводить сообщения о недостижимом коде.•Check xr/xs Assertions (channel assertions) – проверять, что только процесс, в которомописан канал с использованием оператора xr, имеет право на чтение данных изканала. Аналогично, процесс, в котором канал описан с использованием xsоператора, имеет эксклюзивное право на запись данных в канал.65Литература1. Holzmann G. "Spin Model Checker. The Primer and Reference Manual" Addison Wesley,2003, 608 стр.2.
Peterson G. "An O(n log n) Unidirectional Algorithmfor the Circular Extrema Problem"ACM Transactions on Programming Languages and Systems (TOPLAS), v. 4 , i. 4, p. 758– 762, 19823. Dolev D., Klawe M., Rodeh M. "An O(n log n) Unidirectional Distributed Algorithm forExtrema Finding in a Circle" Journal of Algorithms, 3, стр. 245-260, 19824. Lowe G. " Breaking and Fixing the Needham-Schroeder Public-Key Protocol using FDR"Lecture Notes In Computer Science; v. 1055, Proceedings of the Second InternationalWorkshop on Tools and Algorithms for Construction and Analysis of Systems table ofcontents, стр.
147 – 166, 19965. Карпов Ю.Г.. Model checking. Верификация параллельных и распределенных программныхсистем. // БХВ-Петербург, 2009, 520 с.66.
