И.В. Шошмина, Ю.Г. Карпов - Введение в язык Promela и систему комплексной верификации Spin

Введение в язык Promela и системукомплексной верификации SpinИ.В. Шошмина, Ю.Г. КарповСанкт-Петербургский государственныйполитехнический университет– 2009 –СодержаниеПРЕДИСЛОВИЕ ....................................................................................................................................................41.ОБЗОР ЯЗЫКА СПЕЦИФИКАЦИИ МОДЕЛЕЙ PROMELA ...................................................................................71.1.Графическая оболочка XSpin и модель “Hello world”...................................................... 71.2.Типы объектов языка Promela ...............................................................................................

10Типы процессов ......................................................................................................................................................10Типы данных..............................................................................................................................................................12Каналы .......................................................................................................................................................................14Взаимодействие рандеву ....................................................................................................................................16Правило выполнимости ........................................................................................................................................17Выражения................................................................................................................................................................181.3Составные операторы .............................................................................................................

20Блок atomic ..............................................................................................................................................................20Выбор по условию ..................................................................................................................................................21Цикл ............................................................................................................................................................................221.423Некоторые примеры ................................................................................................................. 23ОПИСАНИЕ ВЕРИФИЦИРУЕМЫХ СВОЙСТВ СРЕДСТВАМИ PROMELA И SPIN ..................................................252.1Оператор assert.......................................................................................................................

262.2Метка заключительного состояния (end) ............................................................................... 262.3Метки активного состояния (progress)................................................................................. 272.4Метка принимающего состояния (accept) ......................................................................... 282.5Особый процесс never ...........................................................................................................

28ПРИМЕРЫ ЗАДАЧ ДЛЯ ВЕРИФИКАЦИИ В SPIN ...............................................................................................333.1Протокол выбора лидера в однонаправленном кольце ................................................... 33Описание протокола ............................................................................................................................................33Описание модели протокола на языке Promela ...........................................................................................34Модель алгоритма выбора лидера на языке Promela .................................................................................35Пример симуляции модели выбора лидера .................................................................................................36Верификация базовых свойств ..........................................................................................................................38Проверка LTL формул...........................................................................................................................................383.2Задача о фермере, волке, козе и капусте ..........................................................................

43Описание задачи ...................................................................................................................................................43Модель задачи о волке, козе и капусте на языке Promela ..........................................................................43Поиск решения задачи средствами Spin ........................................................................................................443.3Криптографический алгоритм Нидхама-Шредера ........................................................... 47Описание алгоритма ...........................................................................................................................................47Описание модели на языке Promela ................................................................................................................48Код алгоритма Нидхама-Шредера на языке Promela .................................................................................51Поиск криптографической атаки .....................................................................................................................543.4Задача об обедающих философах .....................................................................................

552Описание алгоритма ...........................................................................................................................................55Описание модели на языке Promela ................................................................................................................56Обнаружение состояния общего голодания .................................................................................................583.5Мир блоков .................................................................................................................................. 59Описание модели на языке Promela ................................................................................................................60Поиск решения задачи средствами Spin ........................................................................................................62ПРИЛОЖЕНИЕ 1.

ПАРАМЕТРЫ СИМУЛЯЦИИ ........................................................................................................63ПРИЛОЖЕНИЕ 2. ПАРАМЕТРЫ ВЕРИФИКАЦИИ БАЗОВЫХ СВОЙСТВ........................................................................65ЛИТЕРАТУРА ......................................................................................................................................................663ПредисловиеПоявление на рынке многоядерных процессоров поставила широкие массы программистовперед проблемой корректного написания параллельных программ. Поэтому умениевыражать свойства поведения параллельных систем и проверять выполнение этих свойств вразработанных программах становится необходимым, фактически, каждому программисту.Данное пособие посвящено описанию программного средства верификации параллельныхпрограмм Spin.

Пакет Spin позволяет:•строить модели параллельных программ (протоколов, драйверов, системлогического контроля и управления) и широкого класса дискретных систем•выразить требуемые свойства их поведения (так называемые “темпоральныесвойства”) и•автоматически (с помощью “push button technique” – “техники нажатия кнопки”)проверить выполнение темпоральных свойств параллельных систем на их моделяхна основе формального подхода.Spin – свободно распространяемый пакет программ для формальной верификации систем,разработанный в Исследовательском Центре Bell Labs Джерардом Холзманном (JerardHolzmann), он широко применяется как в обучении студентов методам верификации, так и впромышленности для формального анализа свойств разрабатываемых протоколов ибортовых систем. Ежегодно проводятся конференции пользователей этого пакета, влитературе широко обсуждаются многочисленные примеры применения Spin дляверификации сложных систем. Международная Ассоциация ACM (Association for ComputingMachinery) наградила программное средство Spin престижной премией ACM Software SystemAward за 2001 г.

В 1983 году этой премией была награждена ОС UNIX, в 1997 г. – Tcl/Tk, в2002 г. – язык Java.Литература по системе Spin на английском языке довольно обширна. Домашняя страницаэтой системы http://spinroot.com/. На этой странице можно найти ссылки на руководства посистеме, ссылки на труды ежегодных конференций по этому продукту. Наиболее полнымописанием системы Spin является монография Gerard J. Holzmann. The Spin Model checker.Авторам неизвестны руководства по системе Spin на русском языке.Мы будем рассматривать Spin не с точки зрения его структуры и реализации, а с точкизрения его использования для верификации, проверки правильности программ. С помощьюсистемы Spin выполняется проверка не самих программ, а их моделей.

Для построениямодели по исходной параллельной программе или алгоритму пользователь (обычновручную) строит представление этой программы на С-подобном входном языке пакета Spin,названном автором Promela (Protocol Meta Language). Это представление –программу наязыке Promela можно считать моделью верифицируемой программы.

Конструкции языкаPromela просты, они имеют ясную и четкую семантику, позволяющую перевести(оттранслировать) любую программу на этом языке в систему переходов с конечным числомсостояний, которая представляет собой модель переходов подлежащей верификациипараллельной программы или алгоритма..Аббревиатура Spin расшифровывается какинтерпретатор программ на языке Promela.SimplePromelaInterpreter–простойSpin может использоваться в двух режимах – как симулятор и как верификатор.