- •Математическая индукция. Принципы простой индукции, модифицированной простой индукции, строгой индукции.
- •1) Доказать, что справедливо s(1);
- •Основные принципы доказательства правильности для блок-схем с использованием индукции. Инварианты цикла при доказательстве правильности.
- •Метод индуктивных утверждений как обобщение метода доказательства правильности с использованием индукции. Верификация программ.
- •Метод индуктивных утверждений.
- •Метод индуктивных утверждений
- •Надежность программных средств
- •Доказательство правильности программы
- •Формализация доказательства с помощью индуктивных утверждений. Множество условий верификации.
- •Аксиоматический подход к доказательству частичной правильности и его идентичность методу индуктивных утверждений.
- •Рекурсивные программы. Доказательство их правильности методом структурной индукции. Рекурсия
- •Метод структурной индукции
- •Моделирование. Природа моделируемых систем. Применение теории сетей Петри. Прикладная и чистая теории сетей Петри.
- •Структура сетей Петри. Способы задания сетей Петри. Графы сетей Петри.
- •Маркировка сетей Петри. Правила выполнения сетей Петри. Пространство состояний сетей Петри.
- •События и условия. Моделирование процесса сетью Петри. Примитивные и непримитивные события. Одновременность и конфликт.
- •Сети Петри для моделирования. Моделирование аппаратного обеспечения сетями Петри (конечные автоматы, эвм с конвейерной обработкой, кратные функциональные блоки).
- •Сети Петри для моделирования. Моделирование программного обеспечения сетями Петри (блок-схемы, обеспечение параллелизма).
- •Сети Петри в решении задач синхронизации: задача о взаимном исключении, задача о производителе/потребителе, задача об обедающих мудрецах, задача о чтении/записи, p- и V-системы и др.
- •Задачи анализа сетей Петри: безопасность, ограниченность, сохранение, активность, покрываемость.
- •Дерево достижимости сети Петри.
- •Использование дерева достижимости для анализа сетей Петри.
- •Матричные уравнения и их использование для анализа сетей Петри.
- •Сети Петри с ограничениями и подклассы сетей Петри.
- •1) Автоматные сети Петри
- •2) Маркированные графы
- •3) Сети свободного выбора
- •4) Правильные сети Петри
- •Расширенные модели сетей Петри (области ограничения, переходы исключающее или, сети со сдерживающими дугами, сети с приоритетами, временные сети)
- •Взаимосвязь мощности моделирования и мощности разрешения сетей Петри
Сети Петри с ограничениями и подклассы сетей Петри.
Временная сеть Петри
Такая сеть позволяет более реалистично отражать процессы в ВС. Во временных сетях каждому переходу tj сопоставляется время τj. Если переход возбуждается, то метки, вызвавшие запуск перехода, покидают входные позиции Pre(tj). Порождение меток в выходных позициях Post(tj) происходит через время τj .
Формальное определение временной сети:
TN = {N, τ},
где N - сеть Петри; τ: T → R0 -функция времён срабатывания, сопоставляющая каждому переходу постоянное время срабатывания; R0 - множество неотрицательных рациональных чисел.
Сеть с приоритетами переходов
Формальное определение:
PRN = {N, PR},
где N - сеть Петри; PR - отношение приоритетности (порядка), задаваемое на множестве переходов Т и определяющее порядок потребления меток возбуждёнными переходами в условиях конфликта за метку.
Временная сеть с приоритетами переходов
Такая сеть объединяет элементы, описанные в рассмотренных выше классах сетей.
Формальное определение:
PRTN = {N, τ, PR}.
Подклассы сетей Петри:
1) Автоматные сети Петри
Автоматная сеть Петри – это сеть Петри, в которой каждый переход может иметь точно один вход и один выход. Автоматная сеть Петри – это сеть Петри С = (P, T, I, O) такая, что для всех T, |I()| = 1 и |O()| = 1.
Некоторые свойства автоматных сетей Петри очевидны.
Прежде всего, автоматные сети Петри – строго сохраняющие. Это означает, что число фишек в такой сети никогда не изменяется, и мы получим, таким образом, конечную систему.
Отсюда следует, что дерево достижимости для автоматной сети Петри является конечным, и, следовательно, все вопросы анализа для автоматных сетей Петри разрешимы.
В автоматных СП легко представить конфликтные ситуации с помощью позиции с несколкими выходами, но нельзя моделировать создание и уничтожение фишек, необходимых для моделирования параллельности, или ожидания, свойственные задачам синхронизации.
2) Маркированные графы
Маркированный граф есть сеть Петри, в которой каждая позиция является входом, для точно одного перехода и выходом точно одного перехода. Иначе говоря, мы можем сказать, что каждая позиция имеет точно один вход и один выход. Маркированный граф есть сеть Петри С = (P, T, I, O), такая, что для каждой P: и .
Маркированные графы двойственны автоматным сетям Петри в теоретико-графовом смысле, т.к. в автоматных СП переходы имеют 1 вход и 1 выход, тогда как в маркированных графах 1 вход и 1 выход имеют позиции.
Маркированные графы могут моделировать параллельность и синхр-ю, но не могут моделировать конфликты и принятие решений, зависящие от данных.
3) Сети свободного выбора
Сеть Петри со свободным выбором есть сеть Петри С = (P, T, I, O) – такая, что для всех T и I() либо I() = {}, либо O(pi) = {}.
Этот подкласс допускает и конфликты автоматных сетей Петри, и параллельность маркированных графов, но в более ограниченном виде, чем в обычных сетях Петри: конфликт появляетс, только когда 1 позиция явл. входом нескольких переходов.
Правильные СП вроде не надо, так что мелким шрифтиком на всякий случай…