Описание тега promela

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

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

через: Википедия