iSpin — написанный на Tcl/Tk [tcltk] вспомогательный графический интерфейс к основной консольной программной утилите системы верификации Spin. Основным элементом графического интерфейса приложения iSpin является главное меню пользователя, обозначенное на экранной форме на рис. 2.1 цифрой 1.
Рис. 2.1. Экранная форма графического интерфейса iSpin с выделенным главным меню пользователя
Главное меню состоит из следующих элементов:
· вкладка «Edit/View» — служит для открытия, редактирования, сохранения и проверки синтаксиса исходного кода модели системы, написанного на языке Promela. Дополнительно на вкладке данного меню можно сформировать представление модели в графическом виде (в виде конечного автомата), а также просмотреть историю всех выполненных пользователем действий;
· вкладка «Simulate/Replay» — служит для выбора режима, настройки, запуска, останова и выполнения по шагам процесса моделирования, а также просмотра его результатов и другой полезной информации;
· вкладка «Verification» — служит для задания верифицируемых свойств модели, настройки параметров и запуска/останова процесса верификации модели, а также просмотра и сохранения его результатов;
· кнопка «Help» — используется для получения справки по программе;
· вкладка «Swarm Run» — используется для установки параметров и запуска большого количества небольших задач верификации в параллельном режиме;
· кнопки «Save Session»/«Restore Session» — служат для сохранения текущей и восстановления сохраненных ранее сессий работы с программой;
· кнопка «Quit» — используется для выхода из программы.
2.1.1. Вкладка редактирования исходного кода модели «Edit/View»
Экранная форма вкладки «Edit/View» программы iSpin представлена на рис. 2.2. Цифрами обозначены следующие элементы пользовательского интерфейса вкладки:
· 1 — верхний ряд кнопок для работы с исходным кодом модели, включающий в себя кнопки: «Open» - кнопка открытия текстового файла с исходным кодом модели; «ReOpen» - кнопка повторной загрузки уже открытого файла модели; «Save»/«Save As» - кнопки сохранения файла модели; «Syntax Check» - кнопка проверки синтаксиса модели на соответствия правилам языка Promela; «Redundancy Check» - кнопка применения к модели специального алгоритма с целью проверки кода на избыточность и генерации советов по возможной оптимизации модели; «Symbol Table» - кнопка генерации таблицы символов модели; «Find» - поиск по исходному коду модели;
Рис. 2.2. Экранная форма вкладки «Edit/View»
· 2 — окно редактирования исходного кода модели на языке Promela;
· 3 — окно графического (в виде конечного автомата) представления процессов системы, описанных в исходном коде с помощью ключевого слова proctype, начального процесса init, а также специальных процессов, получаемых из утверждений о невозможности (never claims), которые используются для проверки свойств модели;
· 4 — окно системного лога, в котором отражаются все действия пользователя в программе и результаты выполнения команд «Syntax Check», «Redundancy Check», «Symbol Table».
2.1.2. Вкладка моделирования «Simulate/Replay»
Экранная форма вкладки «Simulate/Replay» программы iSpin представлена на рис. 2.3. Цифрами обозначены следующие элементы пользовательского интерфейса вкладки:
· 1 — поле выбора режима моделирования и задания ряда настроек моделирования;
Рис. 2.3. Экранная форма вкладки «Simulate/Replay»
· 2 — поле для задания настроек поведения системы в случае заполнения каналов передачи сообщений: если очередь сообщений заполнена, то система может либо блокировать отправителя (blocks new messages), до момента появления свободного места для сообщения, либо терять сообщения (loses new messages);
· 3 — поле для задания настроек фильтрации результатов моделирования. Можно, к примеру, в виде регулярного выражения задать нужные идентификаторы процессов или очередей сообщений;
· 4 — кнопки управления процессом моделирования: «(Re)Run» - запуск/перезапуск моделирования, «Stop» - останов моделирования, «Rewind» - переход на первый шаг моделирования без его перезапуска, «Step Forward»/«Step Backward» - моделирования по шагам (на один шаг вперед и назад, соответственно);
· 5 — окно отображения консольной команды spin с фактическими аргументами, которая выполняется при запуске процесса моделирования;
· 6 — окно с исходным кодом модели на языке Promela, используемой при моделировании;
· 7 — интерактивное окно графического представления последовательности пересылаемых между процессами системы сообщений в формате Message Sequence Chart (MSC) [msc];
· 8 — область вывода результатов моделирования, состоящая из трех отдельных окон.
В системе верификации Spin предусмотрено три режима моделирования:
1. Режим случайного моделирования («Random»), параметром которого является целочисленное значение «зерна» (англ. seed) моделирования. В этом режиме выполнение следующего шага в системе выбирается случайным образом.
2. Режим интерактивного моделирования («Interactive»). В этом режиме выполнение следующего шага в системе выбирается пользователем.
3. Режим моделирования контрпримера («Guided, with trail»). В данном режиме за основу берется контрпример, который может быть сгенерирован в результате процесса верификации, завершившегося ошибкой, и записан в файл с расширением «.trail». Для выбора файла с контрпримером предусмотрено текстовое поле.
Первые два режима обычно используются для быстрого прототипирования модели системы, в то время как третий режим используется для устранения ошибок в модели, выявленных при ее верификации. Для всех режимов можно задать дополнительные параметры: количество пропускаемых от начала шагов моделирования (initial steps skipped), максимальное количество шагов моделирования (maximum number of steps), отслеживание значений переменных в процессе моделирование (Track Data Values). Включение последней опции может заметно затормозить процесс моделирования.
Область вывода результатов моделирования подразделяется на три окна: окно вывода значений переменных на текущем шаге моделирования, окно вывода информации о всех шагах моделирования, окно вывода состояния очередей сообщений на текущем шаге. Значения переменных отображаются только в том случае, если включена опция Track Data Values. Формат отображения: «имя_процесса (идентификатор_процесса): имя_переменной = значение_переменной».
Основная информация о шагах моделирования выводится в центральном окне в виде: «номер_шага: proc идентификатор_процесса (имя_процесса) действие». Большая часть действий процессов имеет следующий формат отображения: «имя_файла_модели: номер_строки_в_файле_модели (state номер_состояния) [ оператор ]». Например, строка вида: «20: proc 5 (node:1) leader0.pml:22 (state 1) [printf('MSC: %d\\n',mynumber)]», означает, что на шаге моделирования под номером 20 процесс с идентификатором 5 и типом node перешел в состояние 1, выполнив оператор «printf('MSC: %d\\n',mynumber)», который стоит в строке № 22 файла модели «leader0.pml». При нажатии в окне на «номер_шага» любой строки можно перейти на соответствующий шаг моделирования, а при нажатии на «номер_строки_в_файле_модели» — на соответствующую строку в файле модели. Перейти на шаг моделирования, в котором происходит отправка сообщения в канал или его прием из канала, можно также нажав на соответствующий графический элемент окна MSC.
В окне вывода состояния очередей сообщений отображается содержимое очередей сообщений всех каналов модели (тип chan в языке Promela) на текущем шаге моделирования.
2.1.3. Вкладка моделирования «Verification»
Экранная форма вкладки «Verification» программы iSpin представлена на рис. 2.4. Цифрами обозначены следующие элементы пользовательского интерфейса вкладки:
Рис. 2.4. Экранная форма вкладки «Verification»
· 1 — область для задания настроек проверяемых у модели свойств безопасности («Safety») и живости («Liveness»);
· 2 — настройка утверждений о невозможности (never claims): для использования утверждений о невозможности необходимо нажать флажок «use claim» и задать имя утверждения в поле ввода.
· 3 — поле настроек режима использования памяти;
· 4 — поле настроек режима обработки автомата, построенного по модели: может использоваться поиск в глубину (флажок «depth-first search») или поиск в ширину (флажок «breadth-first search»). С целью оптимизации процесса верификации для каждого из режимов можно включить использование алгоритма сокращения пространства состояний модели (флажок «partial order reduction»). Включение флажка «report unreachable code» добавляет в результирующий вывод информацию о всех недостижимых состояниях модели;
· 5 — область содержит две кнопки, в результате нажатия на которые отображаются скрытые поля с элементами для настройки дополнительных параметров процесса верификации: параметры обработки ошибок («Show Error Trapping Options») и параметры для задания дополнительных опций верификатора spin («Show Advanced Parameter Settings»).
· 6 — область с кнопками для запуска («Run»), останова («Stop») и сохранения результатов процесса верификации («Save Result in»);
· 7 — окно с исходным кодом модели на языке Promela, используемой для верификации;
· 8 — окно вывода результатов верификации.
Начинать процесс верификации следует с определения режима верификации (проверка свойств безопасности или живости) и настройки параметров выбранного режима. В случае выбора режима проверки свойств безопасности (флажок «safety») доступны следующие дополнительные опции: «invalid endstates (deadlock)» - проверка состояний модели на неправильные конечные состояния (правильным считается состояние, в котором все процессы модели, включая init-процесс, достигли конечного состояния: конца блока описания тела процесса, или заблокировались на операторе, помеченном специальной меткой с префиксом end); «assertion violations» - проверка состояний модели на нарушение пользовательских ассертов (конструкции assert в коде процесса); «xr/xs assertions» - проверка состояний модели на нарушение пользовательских ассертов для эксклюзивного использования канала передачи сообщений на прием (объявления каналов типа xr в коде процесса) или передачу сообщений (объявления каналов типа xs в коде процесса) выделенным процессом.
В случае выбора режима проверки свойств живости (флажок «liveness») доступны следующие основные опции: «non-progress cycles» - проверка модели на циклы без продвижения (потенциально бесконечные вычисления, не помеченные специальной меткой с префиксом progress); «acceptance cycles» - проверка модели на циклы, в которых бесконечно часто посещаются состояния помеченные специальной меткой с префиксом accept; «enforce weak fairness constraint» - включение требования слабой справедливости к вычислениям проверяемой модели (без данной опции в Spin не делается никакого предположения о справедливости вычислений).
