Оглавление
Промела
-
Основы языка Promela
- Promela – язык верификации для моделирования распределенных систем.
- Основан на языке программирования Occam, но имеет дополнительные возможности.
- Включает в себя конструкции для описания процессов, переменных, массивов и потоков управления.
-
Типы данных и переменные
- Байт – величина без знака, может хранить значения от 0 до 255.
- Короткие и целые числа – величины со знаком, различаются диапазоном значений.
- Переменные могут быть объявлены как массивы.
-
Процессы и атомарные конструкции
- Состояние переменной или канала передачи сообщений может быть изменено только процессами.
- Атомарные конструкции позволяют выполнять последовательности инструкций как единое целое.
-
Передача сообщений
- Каналы передачи сообщений используются для передачи данных между процессами.
- Могут быть локальными или глобальными, с буферизацией или без нее.
-
Конструкции потока управления
- В Promela есть три конструкции потока управления: выбор случая, повторение и безусловный переход.
-
Утверждения и сложные структуры данных
- Оператор assert позволяет проверять условия во время проверки с помощью Spin.
- Typedef позволяет вводить новые имена для списков объектов данных.
-
Активные типы клеток и верификация
- Ключевое слово active может активировать proctype в исходном состоянии системы.
- Spin анализирует модели с помощью недетерминированных алгоритмов или генератора случайных чисел.
-
Ключевые слова и рекомендации
- Список зарезервированных ключевых слов и рекомендации по использованию Promela.
- Ссылки на внешние ресурсы и учебные пособия.