- •Математическая индукция. Принципы простой индукции, модифицированной простой индукции, строгой индукции.
- •1) Доказать, что справедливо s(1);
- •Основные принципы доказательства правильности для блок-схем с использованием индукции. Инварианты цикла при доказательстве правильности.
- •Метод индуктивных утверждений как обобщение метода доказательства правильности с использованием индукции. Верификация программ.
- •Метод индуктивных утверждений.
- •Метод индуктивных утверждений
- •Надежность программных средств
- •Доказательство правильности программы
- •Формализация доказательства с помощью индуктивных утверждений. Множество условий верификации.
- •Аксиоматический подход к доказательству частичной правильности и его идентичность методу индуктивных утверждений.
- •Рекурсивные программы. Доказательство их правильности методом структурной индукции. Рекурсия
- •Метод структурной индукции
- •Моделирование. Природа моделируемых систем. Применение теории сетей Петри. Прикладная и чистая теории сетей Петри.
- •Структура сетей Петри. Способы задания сетей Петри. Графы сетей Петри.
- •Маркировка сетей Петри. Правила выполнения сетей Петри. Пространство состояний сетей Петри.
- •События и условия. Моделирование процесса сетью Петри. Примитивные и непримитивные события. Одновременность и конфликт.
- •Сети Петри для моделирования. Моделирование аппаратного обеспечения сетями Петри (конечные автоматы, эвм с конвейерной обработкой, кратные функциональные блоки).
- •Сети Петри для моделирования. Моделирование программного обеспечения сетями Петри (блок-схемы, обеспечение параллелизма).
- •Сети Петри в решении задач синхронизации: задача о взаимном исключении, задача о производителе/потребителе, задача об обедающих мудрецах, задача о чтении/записи, p- и V-системы и др.
- •Задачи анализа сетей Петри: безопасность, ограниченность, сохранение, активность, покрываемость.
- •Дерево достижимости сети Петри.
- •Использование дерева достижимости для анализа сетей Петри.
- •Матричные уравнения и их использование для анализа сетей Петри.
- •Сети Петри с ограничениями и подклассы сетей Петри.
- •1) Автоматные сети Петри
- •2) Маркированные графы
- •3) Сети свободного выбора
- •4) Правильные сети Петри
- •Расширенные модели сетей Петри (области ограничения, переходы исключающее или, сети со сдерживающими дугами, сети с приоритетами, временные сети)
- •Взаимосвязь мощности моделирования и мощности разрешения сетей Петри
Сети Петри для моделирования. Моделирование аппаратного обеспечения сетями Петри (конечные автоматы, эвм с конвейерной обработкой, кратные функциональные блоки).
События и условия.
Представление системы сетью Петри базируется на двух понятиях: событиях и условиях. Под событием понимается действие, имеющее место в системе. Появление события определяет состояние системы, которое может быть описано множеством условий. Условие - это предикат или логическое описание состояния системы. При этом условие может принимать либо значение "истина", либо значение "ложь".
Для того, чтобы событие произошло, необходимо выполнение соответствующих условий, которые называются предусловиями события. Возникновение события может привести к появлению постусловий.
В сети Петри условия моделируются позициями, события - переходами. При этом входы перехода являются предусловиями соответствующего события, выходы - постусловиями. Возникновение события равносильно запуску соответствующего перехода. Выполнение условия представляется фишкой (маркером) в позиции, соответствующей этому условию. Запуск перехода удаляет разрешающие маркеры, представляющие выполнение предусловий и образует новые маркеры, которые представляют выполнение постусловий.
Особенности сетей Петри и систем, моделируемых с их помощью:
- параллелизм, или одновременность (сети Петри удобны для моделирования систем с распределенным управлением).
- асинхронность (в сети Петри отсутствует измерение времени или течение времени. Сеть Петри содержит необходимую информацию для определения возможных последовательностей событий).
- недетерминированность выполнения сети Петри (порядок появления событий один из возможных, выбор запускаемого перехода при нескольких разрешенных осуществляется недетерминировано, то есть случайно).
Запуск перехода и соответствующего события рассматривается как мгновенное событие, и возникновение двух событий одновременно невозможно. Моделируемое таким образом событие называется примитивным, примитивные события мгновенны и неодновременны.
Примитивные и непримитивные события
Непримитивныминазываются такие события, длительность которых не равна 0. Они не являются неодновременными и, следовательно, могут пересекаться во времени.
Непримитивное событие можно представить в виде двух примитивных событий: ”начало не примитивного события”, “конец не примитивного события”, и условия “не примитивное событие происходит”.
Моделирование аппаратного обеспечения ЭВМ
Аппаратное обеспечение (АО) ЭВМ можно моделировать на нескольких уровнях и сети Петри можно использовать для моделирования на каждом из них.
Применение аппарата конечных автоматов
На низком уровне ВС могут быть описаны автоматами.
Автомат – это пятёрка (Q, Σ, Δ, δ, r), где
Q – конечное множество состояний {q1, q2, ..., qk};
Σ – конечный входной алфавит;
Δ – конечный выходной алфавит;
δ: Q x Σ → Q – функция следующего состояния, отображающая текущее состояние и текущий вход в следующее состояние;
r: Q x Σ → Δ – функция выхода, отображающая текущее состояние и текущий вход в выходной символ.
Автоматы часто представляются в виде графов переходов, как на рисунке
Дуга из qi в qj, помеченная a / b, означает, что, находясь в состоянии qi, автомат при входе a перейдёт в состояние qj, выдавая при этом символ b. Формально, это соответствует δ(qi, a) = qj и r(qi, a) = b. Для рис. 5 Σ = {0, 1, R}, Δ = {0, 1, R}
При представлении конечного автомата сетью Петри следует обратить внимание, на связь между внешним миром и сетью Петри. Моделирование взаимодействия возможно несколькими способами. В нашей задаче мы моделируем это взаимодействие с помощью специального множества позиций. Позициями будет представлен каждый входной и выходной символы. Мы допускаем, что из внешнего мира помещается фишка в позицию, соответствующую входному символу, а затем фишка, появившаяся в позиции, соответствующей выходному символу удаляется от туда.
Другой подход: моделирование входов и выходов сети с помощью переходов.
Для определения следующего входного символа из внешнего мира следует выбрать входной переход и запустить его. Сеть Петри ответит запуском соответствующего перехода из множества выходных переходов, связанного с соответствующим выходом. Затем из внешнего мира будет запущен новый входной переход и так далее.
Теперь завершающий переход от конечного автомата к сети Петри. Каждое состояние автомата представим позицией в сети Петри. Текущее состояние отмечается фишкой, все остальные позиции пусты. Теперь для определения переходов из состояния в состояние можно ввести переходы следующим образом. Для каждой пары (состояние и входной символ) мы определяем переход, входными позициями которого являются позиции, соответствующие состоянию и входному символу, а выходными позициями – позиции, соответствующие следующему состоянию и выходному символу.
Для конечного автомата (Q,, Σ, Δ, δ, r) определяем сеть Петри (P, T, I, O) следующим образом:
P = Q ∪ Σ ∪ Δ
Т = {tq, σ / q ∈ Q и σ ∈ Σ}
I(tq , σ) = {q, σ}
O(tq , σ) = {δ(q, σ), r(q, σ)}
Сеть Петри соответствующая конечному автомату, представленному на рис. 5, пока-зана на следующем рисунке:
Сети Петри могут представлять любую систему, представимую автоматом.
ЭВМ с конвейерной обработкой
Сеть Петри является наиболее подходящим средством для проектирования вычисли-тельных систем, состоящих из многих компонент, так как позволяют моделировать параллелизм и довольно просто объединять подсистемы, представленные сетями Петри. Кроме того сети Петри дают возможность моделировать систему на нескольких различных уровнях абстракции, то есть иерархическим образом.
Кратные функциональные блоки
Кратные идентичные функциональные блоки показываются соответствующим числом фишек в позициях.
Эта схема представляет собой очень простой способ введения параллелизма и не рассматривает, того факта, что кратные функциональные блоки могут использовать одновре-менно одинаковые входные регистры. Таким образом максимальный параллелизм в этой схеме может быть не получен. Для этого нужны более сложные схемы и, следовательно, более сложные сети Петри.