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

Присимуляции Spin выводит информацию об одной конкретной траектории выполненияпостроенной модели - графическое представление поведения в виде ДиаграммПоследовательностей Сообщений (Message Sequence Diagrams), возникающих прифункционировании параллельных процессов по данной траектории. Графический интерфейспользователя XSpin визуализирует запуски симуляций и упрощает процесс отладки модели.4Выполняя симуляцию и отладку систем, надо понимать, что никакое количество симуляцийне может доказать свойства модели. Для доказательства свойств модели используетсяверификация – другой режим работы Spin.

Верификатор пытается найти контрпример неправильную, ошибочную траекторию поведения, опровергающую заданное пользователемсвойство, анализируя все возможные поведения модели. Для этого он строит сложнуюконструкцию – синхронное произведение модели переходов анализируемой системы иавтомата Бюхи, задающего все возможные некорректные поведения. В случае нахожденияконтрпримера симулятор Spin демонстрирует его пользователю в управляемом режимесимуляции.

Таким образом, симуляция и верификация в Spin тесно связаны.Разработанные на языке Promela модели отличаются от верифицируемых программ, обычнонаписанных на языках программирования высокого уровня, например, Java или C.Программы на Promela не имеют классов, они представляют плоскую структурувзаимодействующих параллельных процессов, имеют минимум управляющих конструкций.все переменные имеют конечные области определения.

Поэтому такую программу можносчитать моделью анализируемой системы они представляют абстракцию системы, в которойпользователь должен отразить те аспекты и характеристики реальной проверяемой системы,которые значимы для заданных для верификации свойств. Построенная модель можетсодержать траектории, которые не относятся к реализации проверяемой системы в исходномязыке программирования. Например, такие траектории могут включать явнуюспецификацию возможных ситуаций при наихудшем поведении среды, в модели может явноили неявно указываться спецификация свойств справедливости.Описание проверяемой системы на языке Promela должно сохранять существенные свойстваэтой системы. Можно сказать, что качество результата проверки моделей программ,представленных на Promela, полностью зависит от степени адекватности построенноймодели.Таким образом, модель программной системы, верифицируемая с помощью системы Spin, иреальная реализация системы принципиально отличаются.

Верифицируемая модель можетстроиться на этапе начальной разработки структуры системы (при создании прототипа).Окончательная же система, как правило, отличается существенной детализацией:произвольными объемами буферов, наличием вещественных переменных, более богатымспектром управляющих конструкций, динамическим порождением произвольного числапроцессов и т.п..

Достаточно трудно предложить средство автоматического перехода отреализации системы к ее модели в виде программы на языке Promela. Формальных правил“правильного” построения модели по исходной программе нет, и не может быть, этомуможно научиться только на примерах. Одна из целей пособия – дать такие примеры.Построение модели сложной системы на языке Promela, сохраняющей нетривиальныесвойства этой системы, является искусством, которому нужно учиться.Отметим, однако, что в последнее время многие крупные разработчики критического ПО(например, бортовых систем управления для космических и летательных аппаратов), вчастности, фирма Rockwell Collins, используют новую технологию разработки ПО - MDD(Model Driven Development).

В соответствии с этой технологией формальная модель системыявляется первичной: сначала именно формальная модель строится для будущей системы иверифицируется – на ней проверяются все требуемые свойства, и затем эта же модельявляется основой для генерации “ядра” реализации, к которому могут быть добавленыдополнительные функции таким образом, чтобы эти функции не нарушали проверенныхсвойств.Структура пособияПособие состоит из трех частей. В первой части приводится обзор основных средств языкаPromela.

Вторая часть пособия на нетривиальных примерах демонстрирует разработкунескольких моделей. В частности, строятся модели трех программных систем: протокола5выбора лидера, известной старинной логической задачи “фермер, волк, коза и капуста” икриптографического протокола аутентификации Нидхэама-Шредера. Первая системаверифицируется, т.е. показывается, как с помощью системы Spin проверяются те свойства,которые должны соблюдаться в протоколе. Для второй системы верификатор автоматическинаходит нетривиальное решение логической задачи, в третьем примере демонстрируется, какверификатор автоматически находит атаку на криптографический протокол аутентификации,т.е. такое поведение злоумышленника, которое нарушает конфиденциальностькриптографического протокола.

Стоит отметить, что некорректность этого протокола (т.е.возможная стратегия атаки) не были известны в течение более 10 лет. Кроме этих моделейприводятся и комментируются другие интересные модели, на которых можно научитьсяиспользованию системы Spin для верификации ПО различного назначения.Последняя часть пособия – это Приложение. Здесь объясняется, как установить систему Spinна компьютере студента. Система Spin является бесплатно распространяемой и не требуетлицензирования.Изучать пособие нужно, работая на компьютере. Установив систему Spin, студенту следуетстроить примеры, описанные в пособии.

Все приведенные здесь программы – рабочие, ихнужно ввести в поле редактора, запустить и при их анализе пытаться получить те жерезультаты, которые приведены в тексте.Данное пособие разработано при частичной поддержке фирмы Интел по Договору овыполнении работы по модернизации лекционного курса «Верификация параллельныхпрограммных и аппаратных систем», читаемого на факультете Технической кибернетикиСПбГПУ для магистров по направлению 552822 — Распределенные автоматизированныесистемы, (Договор № SPB/R&D/139/ 2006 от 16.11.2006 между Санкт Петербургскогогосударственного политехнического университета и Интел Текнолоджис Инк.).61.

Обзор языка спецификации моделей PromelaЯзык Promela - абстрактный язык спецификации алгоритмов. Абстрагирование направленона то, чтобы с помощью минимальных выразительных средств (параллельные процессы икоммуникация с помощью каналов, простейшие типы данных с конечным числомвозможных значений и простые управляющие структуры) строить такие абстрактные моделиреальных параллельных и распределенных систем, которые легко представляютсяформальной моделью с конечным числом состояний (структурой Крипке и автоматамиБюхи). Таким образом, Promela является не языком реализации систем (языкомпрограммирования), но языком описания моделей распределенных систем.Язык Promela включает примитивы для создания процессов и богатый набор примитивов длямежпроцессного взаимодействия. Базовые блоки моделей в Promela составляют асинхронныепроцессы, каналы сообщений, синхронизирующие утверждения, структурированные данные.В языке также поддерживается спецификация структур недетерминированного управления.Таким образом, Promela содержит некоторые средства, которые отсутствуют в обычных,широко распространенных языках программирования.

Эти средства способствуютконструированию моделей распределенных систем с высоким уровнем абстракции. В то жевремя в языке отсутствует множество возможностей, которые есть в большинстве языковпрограммирования, например, функции, возвращающие значения, указатели на данные ифункции, сложные структуры данных и т. п. В язык намеренно не включено понятиевремени или часов (свойства реального времени не проверяются в системе Spin);отсутствуют операции с плавающей точкой (чтобы ограничиться моделями с конечнымчислом состояний); ограничено количество вычислительных функций. Подобныеограничения делают относительно сложной реализацию в языке Promela, например,вычисления квадратного корня, но относительно простой реализацию, напритмер, клиентсерверного взаимодействия в сети. "Перекос" в сторону средств взаимодействия процессов вязыке объясняется направленностью языка Promela на верификацию именно параллельных ираспределенных систем, в первую очередь синхронизацию и координацию параллельнопротекающих процессов.На практике именно разработка корректной структуры синхронизации и координации дляпрограммного обеспечения параллельных и распределенных систем оказывается гораздоболее сложной и чреватой ошибками, чем разработка последовательных вычислений.Логическая верификация взаимодействия в параллельных системах, несмотря назначительную вычислительную сложность, может быть сегодня выполнена на основе новойтехники верификации “model checking” более надежно и тщательно по сравнению сверификацией последоватедбных вычислительных процедур.