Промела - Promela

ПРОМЕЛА (Процесс или же Протокол мета-языка) это проверка язык моделирования представлен Джерард Дж. Хольцманн. Язык позволяет динамически создавать одновременный процессы для моделирования, например, распределенные системы. В моделях PROMELA связь через каналы сообщений может быть определена как синхронная (т. Е. Рандеву) или асинхронная (т. Е. С буферизацией). Модели PROMELA можно анализировать с помощью Проверка модели SPIN, чтобы убедиться, что смоделированная система обеспечивает желаемое поведение. Реализация проверена с помощью Изабель / ХОЛ также доступен, как часть Компьютерная проверка автоматов проект.^[1] Файлы, написанные в Promela, традиционно имеют .pml расширение файла.

Вступление

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

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

Ссылка на язык

Типы данных

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

Имя	Размер (бит)	использование	Классифицировать
кусочек	1	беззнаковый	0..1
bool	1	беззнаковый	0..1
байт	8	беззнаковый	0..255
mtype	8	беззнаковый	0..255
короткая	16	подписанный	−2¹⁵..2¹⁵ − 1
int	32	подписанный	–2³¹..2³¹ − 1

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

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

 int Икс [10];

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

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

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

 int Икс[3]; Икс[0] = 1; Икс[1] = 2; Икс[2] = 3;

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

Процессы

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

proctype A () {состояние байта; state = 3;}

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

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

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

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

Атомная конструкция

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

атомарные {операторы;}

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

Передача сообщений

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

chan qname = [16] из {коротких}

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

Заявление:

qname! expr;

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

Заявление:

qname? msg;

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

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

порт канала = [0] из {байт}

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

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

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

В PROMELA есть три конструкции потока управления. Они выбор случая, то репетиция и безусловный прыжок.

Выбор корпуса

Самая простая конструкция - это структура выбора. Использование относительных значений двух переменных а и б, например, можно написать:

если :: (a! = b) -> option1 :: (a == b) -> option2fi

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

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

если :: (A == true) -> option1; :: (B == true) -> option2; / * Может прибыть сюда также, если A == true * / :: else -> fallthrough_option; fi

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

если :: значение = 3; :: значение = 4; fi

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

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

Повторение (петля)

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

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

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

Безусловные прыжки

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

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

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

Утверждения

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

assert (любое_булево_условие)

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

Сложные структуры данных

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

 typedef MyStruct {     короткая Поле1;     байт  Поле2; };

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

MyStruct x; x.Field1 = 1;

является действительной последовательностью PROMELA, которая присваивается полю Поле1 переменной Икс Значение 1.

Активные типы

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

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 -> пропустить; :: Chan_data_out! M_DW -> пропустить; od;}; proctype P2 (chan Chan_data_in, Chan_data_out) {do :: Chan_data_in? M_DW -> пропустить; :: Chan_data_out! M_UP -> пропустить; od;}; инициализация {атомарная {запускать P1 (Chan_data_up, Chan_data_down); запустить P2 (Chan_data_down, Chan_data_up); }}

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

Когда Вращение анализирует модель, подобную приведенной выше, он проверит выбор с помощью недетерминированный алгоритм, в котором будут исследованы все варианты исполняемых файлов. Однако когда Spin's симулятор визуализирует возможные непроверенные шаблоны общения, может использовать случайный генератор для разрешения "недетерминированного" выбора. Следовательно, симулятор может не показать плохое выполнение (в примере нет плохого следа). Это иллюстрирует разницу между верификацией и моделированием. Кроме того, также можно сгенерировать исполняемый код из моделей Promela с помощью Refinement.^[2]

Ключевые слова

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

активный
утверждать
атомный
кусочек
bool
перемена
байт
чан
d_step
D_proctype
делать
еще
пустой
включено
фи
полный
идти к
скрытый
если
в соответствии
в этом
int
len
mtype
пустой
никогда
полный
od
из
pc_value
printf
приоритет
прототип
при условии
пробег
короткая
пропускать
тайм-аут
typedef
пока не
беззнаковый
xr
хз

внешняя ссылка

[1] ttps://cava.in.tum.de/templates/publications/promela.pdf

[2] Шарма, Асанкхая. "Исчисление уточнения для Промелы". Инжиниринг сложных компьютерных систем (ICECCS), 2013 18-я Международная конференция по. IEEE, 2013.

[1]

[2]