Promela

PROMELA ( процессов или Метаязык протоколов ) — это верификации язык моделирования , предложенный Джерардом Дж. Хольцманном . Язык позволяет динамически создавать параллельные процессы для моделирования, например, распределенных систем . В моделях PROMELA связь через каналы сообщений может быть определена как синхронная (т. е. рандеву) или асинхронная (т. е. буферизованная). Модели PROMELA можно анализировать с помощью средства проверки моделей SPIN , чтобы убедиться, что смоделированная система обеспечивает желаемое поведение. Также доступна реализация, проверенная с помощью Isabelle/HOL , как часть проекта компьютерной проверки автоматов (CAVA). ^[1]^[2] Файлы, написанные в Promela, традиционно имеют .pml расширение файла .

Введение [ править ]

PROMELA — это язык моделирования процессов, предназначенный для проверки логики параллельных систем. Имея программу в PROMELA, Spin может проверить модель на корректность, выполняя случайное или итеративное моделирование работы моделируемой системы, или может сгенерировать программу на C , которая выполняет быструю исчерпывающую проверку пространства состояний системы. В ходе моделирования и проверок SPIN проверяет отсутствие взаимоблокировок, неуказанных приемов и неисполняемого кода. Верификатор также можно использовать для доказательства правильности системных инвариантов и обнаружения циклов незавершенного выполнения. Наконец, он поддерживает проверку линейных временных ограничений; либо с помощью никогда не-претензий Promela, либо путем прямой формулировки ограничений во временной логике . Каждую модель можно проверить с помощью SPIN при различных предположениях об окружающей среде. Как только правильность модели установлена с помощью SPIN, этот факт можно использовать при построении и проверке всех последующих моделей.

Программы PROMELA состоят из процессов, каналов сообщений и переменных . Процессы — это глобальные объекты, которые представляют параллельные объекты распределенной системы. Каналы сообщений и переменные могут быть объявлены как глобально, так и локально внутри процесса. Процессы определяют поведение, каналы и глобальные переменные определяют среду, в которой выполняются процессы.

Языковая ссылка [ править ]

Типы данных [ править ]

Основные типы данных, используемые в PROMELA, представлены в таблице ниже. Размеры в битах указаны для компьютера PC i386/Linux.

Имя	Размер (бит)	Использование	Диапазон
кусочек	1	без подписи	0..1
логическое значение	1	без подписи	0..1
байт	8	без подписи	0..255
мтип	8	без подписи	0..255
короткий	16	подписано	−2 ¹⁵..2 ¹⁵ − 1
интервал	32	подписано	−2 ³¹..2 ³¹ − 1

Имена bit и bool являются синонимами одного бита информации. А byte — это беззнаковая величина, которая может хранить значение от 0 до 255. shortпесок ints — величины со знаком, которые различаются только диапазоном значений, которые они могут принимать.

Переменные также можно объявлять как массивы. Например, объявление:

 int x [10];

объявляет массив из 10 целых чисел, к которым можно получить доступ в выражениях индексов массива, например:

x[0] = x[1] + x[2];

Но массивы не могут быть пронумерованы при создании, поэтому их необходимо инициализировать следующим образом:

 int x[3];
 x[0] = 1;
 x[1] = 2;
 x[2] = 3;

Индексом массива может быть любое выражение, определяющее уникальное целочисленное значение. Эффект индекса вне диапазона не определен. Многомерные массивы можно определить косвенно с помощью typedef построить (см. ниже).

Процессы [ править ]

Состояние переменной или канала сообщений может быть изменено или проверено только процессами. Поведение процесса определяется объявлением типа proctype . Например, следующее объявляет тип процесса A с одним состоянием переменной:

 proctype A()
 {
     byte state;
     state = 3;
 }

Определение proctype только объявляет поведение процесса, но не выполняет его. Первоначально в модели PROMELA будет выполняться только один процесс: процесс типа init , который должен быть явно объявлен в каждой спецификации PROMELA.

Новые процессы могут быть созданы с помощью оператора run , который принимает аргумент, состоящий из имени proctype , из которого затем создается экземпляр процесса. Оператор run можно использовать в теле определений типов процедур , а не только в начальном процессе. Это позволяет динамически создавать процессы в PROMELA.

Выполняемый процесс исчезает, когда он завершается, то есть когда он достигает конца тела в определении типа процедуры , и все дочерние процессы, которые он начал, завершаются.

Проктип также может быть активным (ниже).

Атомная конструкция [ править ]

Путем префикса последовательности операторов, заключенных в фигурные скобки, с ключевым словом atomic, пользователь может указать, что последовательность должна выполняться как одна неделимая единица, не чередующаяся с другими процессами.

 atomic
 {
     statements;
 }

Атомные последовательности могут быть важным инструментом снижения сложности моделей проверки. Обратите внимание, что атомарные последовательности ограничивают количество чередования, разрешенное в распределенной системе. Трудноразрешимые модели можно сделать управляемыми, помечая все манипуляции с локальными переменными атомарными последовательностями.

Передача сообщений [ править ]

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

chan qname = [16] of {short}

Здесь объявляется буферизованный канал, который может хранить до 16 сообщений типа short ( здесь емкость равна 16).

Заявление:

qname ! expr;

отправляет значение выражения expr в канал с именем qname , то есть добавляет значение в конец канала.

Заявление:

qname ? msg;

получает сообщение, извлекает его из заголовка канала и сохраняет в переменной msg. Каналы передают сообщения в порядке поступления.

Порт встречи можно объявить как канал сообщений с нулевой длиной хранилища. Например, следующее:

chan port = [0] of {byte}

определяет порт встречи, который может передавать сообщения типа byte. Взаимодействие сообщений через такие порты рандеву по определению синхронно, т.е. отправитель или получатель (тот, который прибывает первым на канал), блокируется для претендента, который прибывает вторым (получатель или отправитель).

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

Конструкции потока управления [ править ]

В PROMELA существует три конструкции потока управления. Это выбор падежа , повторение и безусловный переход .

Выбор случая [ править ]

Простейшей конструкцией является структура выбора. используя относительные значения двух переменных a и b Например, , можно написать:

 if
 :: (a != b) -> option1
 :: (a == b) -> option2
 fi

Структура выбора содержит две последовательности выполнения, каждой из которых предшествует двойное двоеточие. Будет выполнена одна последовательность из списка. Последовательность может быть выбрана только в том случае, если ее первый оператор является исполняемым. Первый оператор управляющей последовательности называется защитным .

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

 if
 :: (A == true) -> option1;
 :: (B == true) -> option2; /* May arrive here also if A==true */
 :: else -> fallthrough_option;
 fi

Следствием недетерминированного выбора является то, что в приведенном выше примере, если A истинно, можно выбрать оба варианта . В «традиционном» программировании структуру if – if – else следует понимать последовательно. Здесь if – двойное двоеточие – двойное двоеточие следует понимать как «любой готов», и если никто не готов, только тогда будет другое взято .

 if
 :: value = 3;
 :: value = 4;
 fi

В приведенном выше примере value недетерминировано присваивается значение 3 или 4.

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

Повторение (цикл) [ править ]

Логическим продолжением структуры выбора является структура повторения. Например:

 do
 :: count = count + 1
 :: a = b + 2
 :: (count == 0) -> break
 od

описывает структуру повторения в PROMELA. Одновременно можно выбрать только один вариант. После завершения опции выполнение структуры повторяется. Обычный способ завершить структуру повторения — использовать оператор Break . Он передает управление инструкции, которая следует сразу за структурой повторения.

Безусловные переходы [ править ]

Другой способ разорвать цикл — это goto заявление. Например, можно изменить приведенный выше пример следующим образом:

 do
 :: count = count + 1
 :: a = b + 2
 :: (count == 0) -> goto done
 od
 done:
 skip;

В этом примере переход переходит к метке с именем Done. Метка может появляться только перед оператором. Например, для перехода в конец программы полезен пропуск фиктивного оператора : это заполнитель, который всегда исполняется и не имеет никакого эффекта.

Утверждения [ править ]

Важная языковая конструкция PROMELA, требующая небольшого пояснения, — это оператор утверждения . Заявления формы:

assert(any_boolean_condition)

всегда являются исполняемыми. Если указанное логическое условие выполняется, оператор не имеет никакого эффекта. Однако если условие не обязательно выполняется, оператор выдаст ошибку во время проверок с помощью SPIN .

Сложные структуры данных [ править ]

A PROMELA Определение typedef можно использовать для введения нового имени для списка объектов данных предопределенных или ранее определенных типов. Новое имя типа можно использовать для объявления и создания экземпляров новых объектов данных, которые можно использовать в любом контексте очевидным образом:

 typedef MyStruct
 {
     short Field1;
     byte Field2;
 };

Доступ к полям, объявленным в конструкции typedef , осуществляется так же, как и в языке программирования C. Например:

MyStruct x;
x.Field1 = 1;

является допустимой последовательностью PROMELA, которая присваивает полю Field1 переменной x значение 1 .

Активные проктипы [ править ]

The active Ключевое слово может быть добавлено к любому определению типа процедуры . Если ключевое слово присутствует, экземпляр этого типа процедуры будет активен в исходном состоянии системы. Несколько экземпляров этого типа процедуры могут быть указаны с помощью необязательного суффикса массива ключевого слова. Пример:

 active proctype A() { ... }
 active [4] proctype B() { ... }

Исполняемость [ править ]

Семантика исполняемости обеспечивает в Promela основные средства моделирования синхронизации процессов.

 mtype = {M_UP, M_DW};
 chan Chan_data_down = [0] of {mtype};
 chan Chan_data_up   = [0] of {mtype};
 proctype P1 (chan Chan_data_in, Chan_data_out)
 {
     do
     ::  Chan_data_in  ? M_UP -> skip;
     ::  Chan_data_out ! M_DW -> skip;
     od;
 };
 proctype P2 (chan Chan_data_in, Chan_data_out)
 {
     do
     ::  Chan_data_in  ? M_DW -> skip;
     ::  Chan_data_out ! M_UP -> skip;
     od;
 };
 init
 {
     atomic
     {
         run P1 (Chan_data_up, Chan_data_down);
         run P2 (Chan_data_down, Chan_data_up);
     }
 }

В этом примере два процесса P1 и P2 имеют недетерминированный выбор: (1) входные данные другого процесса или (2) выходные данные другого процесса. Возможны или исполняемы два рукопожатия рандеву , и выбирается одно из них. Это повторяется вечно. Поэтому эта модель не зайдет в тупик.

Когда Spin анализирует модель, подобную приведенной выше, он проверяет выбор с помощью недетерминированного алгоритма, в котором будут исследованы все исполняемые варианты. Spin Однако когда симулятор визуализирует возможные непроверенные модели общения, он может использовать генератор случайных чисел для принятия «недетерминированного» выбора. Поэтому симулятор может не показать плохое выполнение (в примере нет плохого следа). Это иллюстрирует разницу между проверкой и моделированием. Кроме того, из моделей Promela также можно генерировать исполняемый код с помощью Refinement. ^[3]

Ключевые слова [ править ]

Следующие идентификаторы зарезервированы для использования в качестве ключевых слов.

активный
утверждать
атомный
кусочек
логическое значение
перерыв
байт
чан
d_step
D_proctype
делать
еще
пустой
включено
быть
полный
перейти к
скрытый
если
в соответствии
нагревать
интервал
только
мтип
пустой
никогда
полный
из
из
pc_value
печать
приоритет
прототип
предоставил
бегать
короткий
пропускать
тайм-аут
определение типа
пока не
без подписи
хр
хз

Ссылки [ править ]

^ Нойманн, Рене (17–18 июля 2014 г.). «Использование Promela в средстве проверки полностью проверенных исполняемых файлов LTL» (PDF) . VSTTE: Рабочая конференция по проверенному программному обеспечению: теории, инструменты и эксперименты . ЛНКС . Том. 8471. Вена: Шпрингер. стр. 105–114. Архивировано из оригинала (PDF) 7 октября 2015 года.
^ [1] Веб-сайт проекта CAVA
^ Шарма, Асанхая. «Уточняющий расчет для Promela». Инженерия сложных компьютерных систем (ICECCS), 2013 18-я Международная конференция по. ИИЭР, 2013.

Внешние ссылки [ править ]

[1] Нойманн, Рене (17–18 июля 2014 г.). «Использование Promela в средстве проверки полностью проверенных исполняемых файлов LTL» (PDF) . VSTTE: Рабочая конференция по проверенному программному обеспечению: теории, инструменты и эксперименты . ЛНКС . Том. 8471. Вена: Шпрингер. стр. 105–114. Архивировано из оригинала (PDF) 7 октября 2015 года.

[2] [1] Веб-сайт проекта CAVA

[3] Шарма, Асанхая. «Уточняющий расчет для Promela». Инженерия сложных компьютерных систем (ICECCS), 2013 18-я Международная конференция по. ИИЭР, 2013.

[1]

[2]

[3]