исследований, связанные с
доказательством правильности программ (методы доказательства, конструирование
программ и языков, механизация процесса доказательства правильности). Простая
индукция: принцип простой индукции, принцип модифицированной простой индукции,
доказательство высказываний, относящихся к программам для вычислительных машин.
Строгая версия математической индукции: принцип строгой индукции. Обобщенная
индукция: принцип обобщенной индукции. – 2 часа.
Тема 2. Доказательство
правильности блок-схем программ. Основные принципы доказательства
правильности для блок-схем. Дополнительные примеры доказательства правильности
блок-схем программ. Метод индуктивных утверждений (основные определения и
теоремы, описание метода). Сокращенные доказательства правильности.
Формализация доказательства с помощью индуктивных утверждений. – 4 часа.
Тема 3. Доказательство
правильности программ, написанных на обычных языках программирования.
Примеры доказательства правильности программ, написанных на Фортране. Примеры
доказательства правильности программ, написанных на ПЛ/1. Аксиоматический
подход к доказательству частичной правильности. Доказательство частичной
правильности как часть процесса программирования. – 4 часа.
Тема 4. Доказательство
правильности рекурсивных программ. Упрощенный язык программирования для
иллюстрации понятия рекурсии. Структурная индукция. Более трудные примеры
доказательства правильности программ методом структурной индукции. Структурная
индукция для нерекурсивных программ. – 4 часа.
Тема
5. Управляющие структуры и структуры данных. Внешний синтаксис для
управляющих структур: последовательные структуры, структуры с ветвлением,
циклические структуры. Внешний синтаксис структур данных: структуры
поименованных данных (скаляр, массив, запись), структуры непоименованных данных
(список, стек, множество, очередь, дерево, граф). Внутренний синтаксис:
выражения внутреннего синтаксиса, типы данных. – 2 часа.
2. Организация вычислительных
процессов.
Процессы и потоки
Тема 6. Мультипрограммирование. Мультипрограммирование (или многозадачность).
Мультипрограммирование в системах пакетной обработки. Мультипрограммирование в
системах разделения времени. Мультипрограммирование в системах реального
времени. Мультиобработка. – 2 часа.
Тема 7. Планирование процессов и потоков. Понятие “процесс” и “поток”. Создание процессов и
потоков. Планирование и диспетчеризация потоков. Состояние потока. Вытесняющие
и невытесняющие алгоритмы планирования. Алгоритмы планирования, основанные на
квантовании. Алгоритмы планирования, основанные на приоритетах. Смешанные
алгоритмы планирования. Планирование в системах реального времени. Моменты
перепланирования. – 2 часа.
Тема 8. Мультипрограммирование на основе прерываний.
Назначение и типы прерываний. Механизм прерываний. Программные прерывания.
Диспетчеризация и приоретизация прерываний в ОС. Функции централизованного диспетчера
прерываний на примере Windows NT. Процедуры обработки прерываний и текущий процесс.
Системные вызовы. – 2 часа.
Тема 9. Синхронизация процессов и потоков. Цели и средства
синхронизации. Необходимость синхронизации и гонки. Критическая секция. Блокирующие
переменные. Семафоры. Тупики. Синхронизирующие объекты ОС. Сигналы. – 2 часа.
Тема 10. Обмен данными между процессами и потоками. Конвейеры,
именованные конвейеры, очереди сообщений. Способ взаимодействия между
процессами в распределенных системах (в отличие от централизованных). Синхронизация.
Буферизация в примитивах передачи сообщений. Надежные и ненадежные примитивы.
Способы адресации, интерфейсы и протоколы связывания клиента с сервером. – 2
часа.
3. Сети Петри
Тема 11. Сети Петри как
инструмент моделирования систем. Моделирование. Природа систем.Принципы
построения сетей Петри. Структура сетей Петри. Графы сетей Петри. Маркировка сетей
Петри Пространство состояний сетей Петри Алгоритмы поведения сетей Петри. – 4
часа.
Тема 12. Способы реализации сетей Петри. Альтернативные формы
определения сетей Петри. сети
Петри: события и условия, одновременность и конфликт. Моделирование сетями
Петри аппаратного и программного обеспечения ЭВМ. Задачи и методы анализа сетей
Петри. Области применения сетей Петри. . – 4 часа.
II. Темы практических занятий –
17 часов
1. Математическая индукция. – 2 часа.
2. Доказательство правильности блок-схем программ. – 4
часа.
3. Доказательство правильности программ, написанных на
обычных языках программирования. – 2 часа.
4. Рекурсивные программы. Работа со списками. – 2
часа.
5. Доказательство правильности рекурсивных программ. –
2 часа.
6. Управляющие структуры. Доказательство правильности
структурированных программ. – 2 часа.
7. Структуры поименованных и непоименованных данных. –
2 часа.
III. Темы Лабораторных занятий –
17 часов
1. Написание и верификация программ методом
математической индукции. – 4 часа.
2. Проектирование, тестирование и верификация программ
с использованием методики структурного программирования. – 4 часа.
3. Разработка инвариантов для циклических
элементарных программ. Анализ и структурирование схемы программы. – 4 часа.
4. Проектирование сети Петри и исследование алгоритмов
ее поведения.
– 4 часа.
5.
Заключительное занятие. – 1 час.
IV.
Расчетно-графическая работа (7
семестр)
Цель работы:
закрепление теоретических знаний и формирование практических навыков по
верификации программного обеспечения.
Тематика работы: написание программы на языке
высокого уровня и проведение доказательства правильности ее блок-схемы и самой
программы, используя метод математической индукции.
Отчет должен содержать: постановку задачи, исходные данные, блок-схему
программы, тексты программных модулей, описание алгоритмов верификации и выводы
по проделанной работе.
V.
Расчетно-графическая работа (8 семестр)
Цель работы:
закрепление теоретических знаний и формирование практических навыков по
использованию сетей Петри для моделирования вычислительных процессов, а также
приобретение навыков работы с отечественными и зарубежными
информационно-справочным материалом.
Тематика работы: написание программы,
решающей задачу моделирования определенного процесса с использованием сетей
Петри.
Отчет должен содержать: постановку задачи, исходные данные, блок-схему
программы, тексты программных модулей и выводы по проделанной работе.
VI. список литературы
1. Р. Андерсен Доказательство правильности программ.
М.: Мир, 1982.
2. Информатика. Теория и практика структурного
программирования: Методическая разработка. – Новосибирск, изд-во НГТУ, 1999.
3. Лингер Р., Миллс Х., Уитт Б. Теория и практика
структурного программирования. /Пер. с англ., М.: Мир, 1982.
4. Олифер В. Г., Олифер Н.А. Сетевые операционные
системы. – СПб.: Питер, 2001.
5. Олифер В. Г., Олифер Н.А. Компьютерные сети.
Принципы, технологии, протоколы. – СПб.: Питер, 1999.
6. Дж. Питерсон Теория сетей Петри и моделирование
систем. – М.: Мир, 1984.
Приложение.
Список вопросов к экзамену (7 семестр).
1.
Основные направления исследований,
связанные с доказательством правильности программ .
2.
принцип простой индукции
3.
принцип модифицированной простой индукции
4.
Строгая версия математической
индукции: принцип строгой индукции
