НОВОСИБИРСКИЙ ГОСУДАРСТВЕННЫЙ ТЕХНИЧЕСКИЙ УНИВЕРСИТЕТ
ФАКУЛЬТЕТ ПРИКЛАДНОЙ МАТЕМАТИКИ И ИНФОРМАТИКИ
КАФЕДРА ПАРАЛЛЕЛЬНЫХ ВЫЧИСЛИТЕЛЬНЫХ ТЕХНОЛОГИЙ
“УТВЕРЖДАЮ”
Декан ФПМИ
“___ ”____________2009 г.
РАБОЧАЯ ПРОГРАММА УЧЕБНОЙ ДИСЦИПЛИНЫ
КОМПЬЮТЕРНЫЕ ТЕХНОЛОГИИ
В ПРИКЛАДНОЙ МАТЕМАТИКЕ И ИНФОРМАТИКЕ
ООП: 010500 – прикладная математика и информатика;
квалификация – магистр прикладной математики и информатики
Факультет Прикладной математики и информатики
Курс 5 и 6
Семестр 10 и 11
Лекции 35 часов
Самостоятельная работа 36 часов
Экзамен 11 семестр
Зачет 10 семестр
Всего 71 час
Новосибирск 2009
Рабочая программа составлена на основании государственного образовательного стандарта по направлению 010500 «Прикладная математика и информатика», утвержденный приказом Министерства образования Российской федерации от 01.01.2001г. 201ен/маг.
Рабочая программа обсуждена на заседании кафедры Параллельных вычислительных технологий «25» апреля 2006 г. (протокол № 26)
Шифр дисциплины: ОПД. Р.02
Программу составил: доц., к. ф.-м. н.
Заведующий кафедрой ПВТ проф., д. т.н.
Ответственный за основную
заведующий кафедрой ПМт проф., д. т.н.
1. Внешние требования
Требования ГОС к требования к обязательному минимуму содержания основной образовательной программы подготовки магистра по направлению 510200 «Прикладная математика и информатика»
Таблица 1
Индекс дисциплины | Содержание учебной дисциплины «Формальные модели параллельных вычислений» | Часы |
СДМ.00 | Специальные дисциплины | 800 |
Состав и содержание специальных дисциплин определяется требованиями специализации магистра при реализации конкретной магистерской программы |
1.3. Квалификационные требования
Магистр прикладной математики и информатики подготовлен к деятельности, требующей углубленной фундаментальной и профессиональной подготовки, в том числе к научно-исследовательской работе в областях, использующих методы прикладной математики и компьютерные технологии; созданию и использованию математических моделей процессов и объектов; разработке и применению современных математических методов и программного обеспечения для решения задач науки, техники, экономики и управления; использованию информационных технологий в проектно-конструкторской, управленческой и финансовой деятельности. Магистр прикладной математики и информатики подготовлен к научно-педагогической деятельности при условии освоения им соответствующей образовательной программы педагогического профиля.
7.1.1. Общие требования к уровню подготовки магистра прикладной математики и информатики определяются содержанием аналогичного раздела требований к уровню подготовки бакалавра и требованиями, обусловленными специализированной подготовкой. Требования к уровню подготовки бакалавра изложены в п.7 государственного образовательного стандарта высшего профессионального образования бакалавра по направлению 010500 - Прикладная математика и информатика. (см. ниже)
Требования, обусловленные специализированной подготовкой магистра прикладной математики и информатики, включают:
владение навыками самостоятельной научно-исследовательской деятельности, требующей широкого образования в соответствующем направлении;
умения:
Выпускник должен обладать знаниями и умениями, соответствующими его степени, указанной п.1.3 настоящего стандарта и магистерской программе, по которой он проходил обучение.
7.1.3. Специальные требования к подготовке выпускника магистратуры по научно-исследовательской части специализированной подготовки определяются вузом.
Требования государственного образовательного стандарта (ГОС) по специальности 010500 «Прикладная математика и информатика» для бакалавра прикладной математики и информатики, раздел 7.1.1:
Бакалавр прикладной математики и информатики:
должен обладать:
теоретическими знаниями и практическими навыками, соответствующими основной образовательной программе подготовки настоящего государственного образовательного стандарта.
должен знать и уметь использовать:
· основы теории алгоритмов и ее применения, методы построения формальных языков, основные структуры данных, основы машинной графики, архитектурные особенности современных ЭВМ;
· синтаксис, семантику и формальные способы описания языков программирования, конструкции распределенного и параллельного программирования, методы и основные этапы трансляции; способы и механизмы управления данными;
иметь опыт:
· работы на различных типах ЭВМ, применения стандартных алгоритмических языков, использования приближенных методов и стандартного программного обеспечения для решения прикладных задач, пакетов прикладных программ и баз данных, средств машинной графики, экспертных систем и баз знаний.
должен:
· обладать знаниями и умениями, позволяющими применять современные математические методы и программное обеспечение для решения задач науки, техники, экономики и управления и использования информационных технологий в проектно-конструкторской, управленческой и финансовой деятельности.
· быть способен к совершенствованию своей профессиональной деятельности в области прикладной математики и информатики.
2. Особенности (принципы) построения дисциплины
Таблица 2
Особенность (принцип) | Содержание |
Основание для введения дисциплины в учебный план направления | Стандарт направления, решение уч. совета ФПМИ от 01.01.2001 № протокола 6. |
Адресат дисциплины | Студенты по направлению: 010500 – Прикладная математика и информатика |
Главная цель дисциплины | Обеспечение базы теоретической и практической подготовки в области спецификации и верификации программ – в том числе параллельных, приобретение знаний, необходимых для изучения последующих дисциплин и самостоятельной исследовательской работы. Обеспечение базы теоретической и практической подготовки в области построения математических моделей современного программного обеспечения, языкам их спецификации, алгоритмам и инструментальным средствам их верификации. |
Ядро дисциплины | Понятие о синтаксисе и семантике программ, логические спецификации программ, логические сервисы – верификаторы моделей и дедуктивная верификация, автоматизация верификации программ. |
Требования к начальной подготовке, необходимые для успешного освоения дисциплины | 1. Необходимы знания по дискретной математике, математической логике и теории алгоритмов. 2. Базовые знания по императивному и параллельному программированию. 3. Необходимы знания и опыт по программированию на компьютере на императивных языках (Си, Паскаль). 4. Опыт работы на персональном компьютере. |
Уровень требований по сравнению со Стандартом | Соответствует требованиям Стандарта |
Объем дисциплины в часах | 35 часов лекций, 36 часов самостоятельных занятий (индивидуальные лабораторные работы, курсовые работы и курсовой проект). |
Основные понятия дисциплины | Формальные спецификации программ, верификация моделей программ (model checking) и верификаторы моделей SMV и SPIN, дедуктивная верификация и дедуктивные сервисы (proof assistance) SLAM и Z3. |
Обеспечение последующих дисциплин образовательной программы | Курсовое и дипломное проектирование. |
Практическая часть дисциплины | Практическая часть дисциплины содержит индивидуальные лабораторные работы, цель которых – получить опыт реализации основных алгоритмов верификации, а так же базовые навыки использования существующих инструментальных средств (верификатора моделей SMV и дедуктивного верификатора SLAM). |
Направленность дисциплины на развитие общепредметных, общеинтеллектуальных умений, обладающих свойством переноса, направленность на саморазвитие | Обобщение, анализ, синтез, классификация, абстрагирование, моделирование, выделение главного. |
Дисциплина и современные информационные технологии | Значение математических средств моделирования, спецификации и верификации программ и систем для критического с точки зрения безопасности программного обеспечения. |
3. Цели учебной дисциплины
После изучения дисциплины студент будет
Таблица 3
Номер цели | Содержание цели |
иметь представление: | |
1 | о классификации логических языков спецификаций программ; |
2 | о дедуктивном подходе к верификации последовательных программ; |
3 | о верификации параллельных программ на моделях. |
знать | |
4 | основные понятия математической логики как-то: модель, аксиоматическая система, дерево доказательства, теория, полнота, аксиоматезируимость и разрешимость теории; |
5 | основные теоремы и алгоритмы для пропозициональной логики (разрешимость, табличную аксиоматезируемость, алгоритм Дэвиса-Путнам); |
6 | метод резолюций для логики первого порядка; |
7 | понятия частичной и тотальной корректности последовательных программ, операционную и аксиоматическую семантику последовательных программ, теорему непротиворечивости аксиоматической семантики последовательных программ, метод Флойда-Хоара доказательства частичной корректности последовательных программ; |
8 | синтаксис и семантику пропозициональной темпоральной логики (логики дерева вычислений CTL и логики линейного времени LTL), прогматику использования CTL и LTL для спецификации и верификации параллельных программ; |
9 | методы проверки пропозициональной темпоральной логики на моделях как основу современно автоматической верификации параллельных программ |
уметь: | |
10 | специфицировать на подходящем логическом языке последовательные и параллельные программы; |
11 | доказывать методом Флойда-Хоара частичную и тотальную корректность специфицированных последовательных программ |
12 | устанавливать методом проверки на моделях свойства типа безопасности и прогресса параллельных программ. |
иметь опыт: | |
13 | работы с верификатором моделей SMV. |
4.Содержание курса
Структура учебной дисциплины
Таблица 4
Лекционные занятия (34 час)
Блок, модуль, раздел, тема | Часы | Ссылки на цели |
Семестр № 10 | ||
Воспоминания о теории множеств и теории формальных языков: основные понятия, определения, свойства и теоремы. | 2 | 4 |
Язык математической логики, его синтаксис и семантика. Классификация логик: пропозициональные, логики 1-ого, 2-ого и высших порядков. | 2 | 1, 2, 4 |
Пропозициональная логика: табличная аксиоматизация и алгоритм Дэвиса-Путнама. | 2 | 5 |
Основы автоматического доказательства теорем. Стратегии поиска доказательства. Использование разрешающих процедур. Проверка моделей. | 2 | 2, 3 |
Логика дерева вычислений, ее синтаксис и семантика. Представление критических свойств безопасности и живости в логике дерева вычислений. Метод проверки моделей для доказательства свойств систем с конечным числом состояний. | 3 | 1, 2, 8, 9, 10, 12 |
Верификатор моделей программ SMV. | 6 | 12, 13 |
Семестр № 11 | ||
Верификатор моделей SPIN (в сравнении с SMV). | 2 | 12, 13 |
Воспоминания об основных теоремах логики первого порядка (Теорема Лёвенгейма-Скулема о счетной модели, теорема Гёделя о полноте, теорема компактности Мальцева). Метод резолюций для логики первого порядка. | 3 | 1, 6 |
Основы верификации последовательных программ. Логика Хора для модельного языка, ее непротиворечивость. Генерация условий корректности. | 3 | 1, 2, 7, 10, 11 |
Дедуктивный верификатор SLAM и логический сервис Z3. | 8 | 13 |
Обзор систем и инструментальных средств дедуктивной верификации и логических сервисов (Simplify, Vampire, PVS, HOL) | 2 | 1, 2, 3 |
Таблица 5
Индивидуальные лабораторные (расчетные) работы (36 часов)
Выполняются на самостоятельно на персональном компьютере.
Темы | Решая задачи, студент: | Ссылки на цели курса | Часы |
Семестр № 10 | |||
Решение головоломок с использованием логики дерева вычислений LTL и верификатора моделей SMV. | приобретает первоначальные навыки спецификации свойств на языке LTL и работы с верификатором моделей SMV. | 1, 2, 8, 9, 10, 12, 13 | 9 |
Семестр №11: курсовой проект «Разработка, спецификация и верификация свойств безопасности и прогресса для варианта альтернирующего битового протокола» состоит из трех лабораторных работ. | |||
Разработка и спецификация варианта альтернирующего битового протокола. | знакомится с протоколами распределенных систем, методами их представления и спецификации. | 1, 10 | 9 |
Верификация свойств функций, используемых процессами варианта альтернирующего битового протокола. | приобретает навыки доказательства свойств последовательных программ методом Флойда-Хоара. | 1, 2, 7, 10, 11 | 9 |
Доказательство свойств безопасности и прогресса с использованием верификатора моделей SMV для варианта альтернирующего битового протокола. | Закрепляют навыки использования верификатором моделей SMV. | 1, 3, 9, 10, 12, 13 | 9 |
5. Учебная деятельность
В течение 11 семестра каждый студент выполняет 5 индивидуальных лабораторных работ на персональном компьютере (на одном или двух языках LISP и ML) и сдаёт их преподавателю в индивидуальном порядке.
6. Правила аттестации студентов по учебной дисциплине
Для аттестации студентов используется балльно-рейтинговая система. В десятом семестре рейтинг студента определяется рейтинг студента определяется сумма баллов за работу в семестре за курсовую лабораторную работу (текущий рейтинг) и баллов, полученных в результате и устного опроса во время зачета. В одиннадцатом семестре рейтинг студента определяется сумма баллов за работу в семестре за лабораторные работы (текущий рейтинг), баллов за защиту курсового проекта (основанного на выполненных лабораторных работ) и баллов, полученных в результате итоговой аттестации (экзамен). Подробнее – см. изменения программы.
7. Список литературы
7.1. Основная литература
1. , , Проценко логика в программировании. Обзор. М. Мир, 1991.
2. Наука программирования, гл.1 Высказывания, гл.3 Система естественного вывода, гл.4 и гл.6-11. М., Мир, 1984.
3. Ершов логика, гл.1, гл.2 и гл.4. М., Наука, 1987.
4. Ball T, Cook B., Levin V. and Rajamani S. K. SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft. Lecture Notes in Computer Science, v.2999, 2004, p.1-20.
5. Huth M. and Ryan M. Logic in Computer Science. Cambridge University Press, 2004.
7. Дополнительная литература
6. , , Ии К. О программных логиках - просто. В сб. Системная информатика, Новосибирск, Наука, 2003.
7. , Рякин методы верификации программ, гл.1-5 и гл.7. М., Радио и связь, 1988.
8. Detlefs D, Nelson G., and Saxe J. B. Simplify: A theorem prover for program checking. J. ACM 52(3), 2005, p.365-473.
8. Контролирующие материалы для аттестации студентов по учебной дисциплине
Экзаменационные вопросы
Основные понятия теории множеств теории множеств и теории формальных языков. Язык математической логики, его синтаксис и семантика. Классификация логик: пропозициональные, логики 1-ого, 2-ого и высших порядков. Пропозициональная логика и ее табличная аксиоматизация и алгоритм Дэвиса-Путнама. Основы автоматического доказательства теорем: стратегии поиска доказательства, использование разрешающих процедур. Проверка моделей. Темпоральные логики CTL и LTL, b[ синтаксис и семантика. Представление критических свойств безопасности и живости в логиках CTL и LTL. Метод проверки моделей для CTL доказательства свойств систем с конечным числом состояний. Общее описание верификатора моделей программ SMV. Общее описание верификатора моделей SPIN. Классические теоремы для логики первого порядка (теорема полноты, компактности, неполноты): формулировки и использование в верификации программ. Метод резолюций для логики первого порядка. Логика Хора для модельного языка, ее непротиворечивость. Генерация условий корректности. Общее описание дедуктивного верификатора SLAM. Краткая характеристика средств дедуктивной верификации и логических сервисов (Simplify, Vampire, PVS, HOL)Образец экзаменационного билета
Министерство образования РФ НОВОСИБИРСКИЙ ГОСУДАРСТВЕННЫЙ ТЕХНИЧЕСКИЙ УНИВЕРСИТЕТ | Экзаменационный билет № ___ По дисциплине «Компьютерные технологии в прикладной математике и информатике» Факультет ФПМИ Курс 5 |
1 . Классические теоремы для логики первого порядка (теорема полноты, компактности, неполноты): формулировки и использование в верификации программ.2 . Общее описание верификатора моделей программ SMV.3 . Задача.Составил Шилов г. |
Задача
к экзаменационному билету № ___
· Специфицировать на языке логики дерева вычислений CTL невозможность одновременного доступа к общей переменной двух параллельных процессов. |
Дополнения и изменения к рабочей программе на 20 /20 учебный год
В рабочую программу вносятся следующие изменения: |
Рабочая программа пересмотрена и одобрена на заседании кафедры «___» ______ 200 г.
Заведующий кафедрой
«___»__________20 г.
