Определения по курсу Верификация моделей программ (1161286), страница 2

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 2)

– множество значений переменных. Собственно, это и есть подстановка.

Эффект –

Графы программ (статическая семантика)

, где:

• – множество точек, исходные (начальные) точки

• – множество действий

• – отношение переходов, – это фактически страж оператора

• – функция эффекта

• – начальное условие

Нотация: означает

Принцип получения TS из PG

• Состояние: точка l + значение данных

• Начальное состояние: начальная точка + все значения данных, удовлетворяющие .

• Атомарные высказывания в TS

  • находимся в точке программы

  • значение переменной x принадлежит некоторому множеству , и это множество является подмножеством множеств значений этой переменной

• Если истинно в , то строим отношение переходов как

Система переходов графов программ TS(PG) над переменными описывается сигнатурой

, где:

• (состояние: точка l + значение данных )

• (множество начальных состояний системы переходов описывается как множество состояний, в которых точка программы принадлежит начальным точкам, а на подстановках выполняется начальное условие графа программы)

• (объединение множества точек программы и всевозможных булевых высказываний над переменными программы)

• (состояния размечаются высказыванием о точке программы, в которой мы находимся и всеми высказываниями из множества всевозможных высказываний, которые верны в этой подстановке)

• задается правилом: если истинно в (в графе программы есть дуга из в со стражем и действием и в некоторой подстановке выполняется страж ), то строим отношение переходов как

Чередование (интерливинг)

• Обоснование

Эффект от параллельного выполнение независимых действий α и равен эффекту от их последовательного выполнения в произвольном порядке

• Символьная запись

• – бинарный оператор чередования

• + – оператор недетерминированного выполнения

• ; – оператор последовательного выполнения

Чередование систем переходов

Пусть – две системы переходов

Определим их чередование как , а отношение перехода определяется правилами:

и

Чередование графов программ

Пусть

Граф определим как

Где отношение перехода определяется правилами

и

И эффект , если

Параллелизм и рандеву

• распределённые программы выполняются параллельно

• в распределённой программе нет разделяемых переменных

Передача сообщений в распределённых программах

• синхронная передача сообщений (рандеву, без буферизации)

• асинхронная передача сообщений (с буферизацией)

Синхронный обмен сообщениями

• Процессы вместе выполняют синхронизированные действия

• Взаимодействие процессов - одновременно

Рандеву систем переходов

• – набор синхронизированных действий.

  • действия из H должны быть синхронизированы

  • действия не из H независимы и могут чередоваться

Тогда , где

• определяется как:

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

• рандеву для : (а вот это – ключевой момент определения: переход из пары состояний происходит только в том случае, когда оба процесса должны что-то делать одновременно – например, прием-передачу информации в синхронном режиме)

Синхронный параллелизм

• Тогда

• определяется как: (тот же комментарий, что и для определения рандеву систем переходов, для случая рандеву)

Promela

Ключевые моменты

• У моделей – конечное число состояний (потенциально бесконечные элементы моделей в Promela ограничены).

  • Гарантирует разрешимость верификации

  • Не гарантирует конечное число вычислений

• Асинхронное выполнение процессов

  • Нет глобальных часов

  • По умолчанию отсутствует синхронизация разных процессов

• Недетерминированный поток управления

  • Абстракция от деталей реализации

• Понятие выполнимости оператора

  • С любым оператором связаны понятия предусловия и эффекта

  • Оператор выполняется (производя эффект)только если выполнено предусловие, в противном случае он заблокирован

  • Пример: q?m – если канал не пуст, получаем из него сообщение, иначе ждем.

  • Присваивания и printf выполняются всегда. Остальное выполняется, если его значение не 0.

• Три типа объектов

  • Процессы

  • Глобальные и локальные объекты данных

  • Каналы сообщений

Число состояний модели конечно, так как

• Число активных процессов конечно (256)

• У каждого процесса – ограниченное число операторов

• Диапазон типов данных ограничен

• Размер всех каналов сообщений ограничен

Недетерминизм

Выполнимость операторов: псевдооператоры

• skip – всегда выполним, без эффекта, эквивалент выражения (1)

• true = skip

• run – 0, если при создании процесса превышен лимит, _pid (ид. процесса) в противном случае

• assert – всегда выполним, не влияет на состояние системы, SPIN сообщает об ошибке, если выражение в assert = 0

Каналы сообщений

• Используются для передачи сообщений между процессами

• Бывают двух типов: буферизованные (асинхронные) и небуферизованные (синхронные, рандеву)

Inline определения

• Среднее между макросом и процедурой

• Именованный фрагмент кода с параметрами

• Не функция – не возвращает значения

Все варианты оператора IF должны быть описаны явно, иначе процесс блокируется.

eval(x) – отображает значение x на константу

Alternating Bit Protocol (ABP)

• Два процесса, отправитель и получатель

• К каждому процессу добавляется один бит

• Получатель сообщает о доставке сообщения, возвращая бит отправителю

• Если отправителю убедился в доставке сообщения, он посылает новое, изменяя значение бита

• Если значение бита не изменилось, получатель считает, что идет повтор от сообщения

Характеристики

Список файлов лабораторной работы