Редактирование: ВПнМ/Теормин
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
ПРЕДУПРЕЖДЕНИЕ: Длина этой страницы составляет 88 килобайт. Страницы, размер которых приближается к 32 КБ или превышает это значение, могут неверно отображаться в некоторых браузерах. Пожалуйста, рассмотрите вариант разбиения страницы на меньшие части.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 1008: | Строка 1008: | ||
=== Система Spin. Процесс моделирования и верификации при помощи системы Spin. Конечность моделей на Promela. Асинхронное выполнение моделей. Недетерминированный поток управления. Понятие выполнимости оператора. === | === Система Spin. Процесс моделирования и верификации при помощи системы Spin. Конечность моделей на Promela. Асинхронное выполнение моделей. Недетерминированный поток управления. Понятие выполнимости оператора. === | ||
- | |||
- | |||
- | '''Верификация программы на модели''' | ||
- | * Мы хотим задавать, как система устроена и как она должна быть устроена | ||
- | * Таким образом, нужно две нотации: | ||
- | ** чтобы описать поведение (устройство системы) | ||
- | ** чтобы описать требования (свойства правильности) | ||
- | * Верификатор: | ||
- | ** проверяет, что устройство системы удовлетворяет свойствам правильности | ||
- | ** выбранная нотация гарантирует разрешимость проверки правильности любого свойства любой модели | ||
- | * Все держится на трех китах | ||
- | ** ''SPIN'' – Simple Promela Interpreter | ||
- | *** верификация | ||
- | *** моделирование | ||
- | ** ''Promela'' – Process Meta Language - описание поведения модели | ||
- | *** недетерминированный язык с охраняемыми командами | ||
- | *** задача языка – разрешить описывать такие модели, которые могут быть верифицированы | ||
- | ** ''LTL'' – Linear Temporal Logic - описание свойств | ||
- | |||
- | '''Конечность моделей на Promela''' | ||
- | * У моделей – конечное число состояний (потенциально бесконечные элементы моделей в Promela ограничены) | ||
- | ** гарантирует разрешимость верификации | ||
- | * Почему число состояний конечно? | ||
- | ** Число активных процессов конечно (от 0 до 255) | ||
- | ** У каждого процесса – ограниченное количество операторов | ||
- | ** Диапазоны типов данных ограничены | ||
- | ** Размер всех каналов сообщений ограничен | ||
- | |||
- | '''Асинхронное выполнение моделей''' | ||
- | * нет глобальных часов | ||
- | * по умолчанию синхронизация отсутствует | ||
- | |||
- | '''Недетерминированный поток управления''' | ||
- | * абстракция от деталей реализации | ||
- | * Два уровня недетерминизма | ||
- | ** внешний (выбор процесса) | ||
- | *** процессы выполняются параллельно и асинхронно (между двумя последовательными операторами одного процесса может быть сколь угодно длинная пауза) | ||
- | *** произвольная диспетчеризация процессов | ||
- | *** выполнение операторов разных процессов происходит в произвольном порядке (основные операторы выполняются атомарно) | ||
- | * внутренний (выбор действия в процессе). | ||
- | ** в теле одного процесса также допускается недетерминированное ветвление | ||
- | |||
- | '''Понятие выполнимости оператора''' | ||
- | * с любым оператором связаны понятия предусловия и эффекта | ||
- | * оператор выполняется (производя эффект), только если предусловие истинно, в противном случае он заблокирован | ||
- | ** Пример 1: ''q?m''; если канал ''q'' не пуст, читаем из него сообщение, иначе ждём | ||
- | ** Пример 2: (''x > y) -> y++''; процесс будет заблокирован до тех пор, пока ''x'' не станет больше ''y''. После этого ''y'' увеличится на единицу. | ||
- | |||
=== Язык Promela. Основные компоненты модели на языке Promela. Процессы, локальные и глобальные объекты данных, каналы сообщений. === | === Язык Promela. Основные компоненты модели на языке Promela. Процессы, локальные и глобальные объекты данных, каналы сообщений. === | ||