rpd000012698 (1010444), страница 2
Текст из файла (страница 2)
- 17. Формальные логические исчисления и аксиоматические теории, их полнота и непротиворечивость
- 18. Вычислимые функции и модели вычисления
- 19. Машины Тьюринга
- 20. Лямбда-исчисление Чёрча
- 21. Многосортные алгебры, решётки, категории
- 22. Шкалы и модели Крипке, семантика “возможных миров
- 23. Ранние подходы к доказательной верификации программ
- 24. Аксиоматика Флойда-Хоара
- 25. Логика PDL (Propositional Dynamic Logic)
- 26. Язык PROMELA и его применение для верификации моделей процессов
- 27. Автоматы Бюхи
- 28. Линейная временная логика LTL и её применение для верификации
- 29. Ветвящаяся временная логика CTL и её применение для верификации
- 30. F-логика и формализация объектно-ориентированных программ
- 31. Диаграммы UML и F-логика
- 32. Верификатор SPIN, назначение и основные функции
- 33. Анализатор моделей NuSMV
- 34. Символический верификатор моделей SVM
- 35. Статический анализатор моделей программ для языка C BLAST
- 36. Java-следопыт JPF (Java Pathfinder)
- 37. Платформа CHESS
- 38. Концепция верификации программ путём “символьного выполнения”
- 39. CREST: генератор и драйвер тестов для интерпретации и анализа программ на языке C
- 40. CATG: драйвер тестов для интерпретации и анализа программ на языке Java
- 41. Концепция верификации программ путём “абстрактной интерпретации"
- 42. Определение понятия процесса
- 43. Проблемы эквивалентности процессов
- 44. Наблюдаемая конгруэнции
- 45. Процессы с передачей сообщений
- 46. Примитивы и алгебраические операторы языка CSP
- 47. Денотационные семантические модели языка CSP
- 48. Модель трасс процессов
- 49. Модель устойчивых ошибок
- 50. Модель устойчивых ошибок/расхождения процессов
- 51. Инструменты для анализа моделей процессов на языке CSP (refinement checking)
- 52. Исчисление процессов CCS Р. Милнера
- 53. П-исчисление Р. Милнера
- 54. Язык LOTOS
- 55. Язык Circus и его использование при проектировании программ
- 56. Подходы к формализации сложности вычислений
- 57. Понятие сигнализирующей функции
- 58. Аксиомы Блюма для сигнализирующих функций
- 59. Проблемы “ускорения” и “сжимания” вычислимых функций
- 60. Теорема о нижней грани и теоремы о сжимании
- 61. Понятие массовой задачи и сложности её вычисления, классы задач P и NP
- 62. Решение массовой задачи недетерминированной машиной Тьюринга
- 63. Понятие полиномиальной сводимости, определение класса NP-полных задач
- 64. Примеры NP-полных задач
-
Лекции
| № п/п | Раздел дисциплины | Объем, часов | Тема лекции | Дидакт. единицы |
| 1 | 1.1.Введение в дисциплину | 4 | Сущность, цели и направления формализации технологий программной инженерии | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15 |
| 2 | 1.1.Введение в дисциплину | 4 | Логико-математические и алгебраические основы “формальных методов” | 16, 17, 18, 19, 20, 21, 22 |
| 3 | 1.2.Формализованный анализ и оценка программ и моделей программ | 2 | Верификация последовательных программ | 23, 24, 25 |
| 4 | 1.2.Формализованный анализ и оценка программ и моделей программ | 2 | Формальная верификация путём “проверки моделей” (model checking) | 26, 27, 28, 29, 30, 31 |
| 5 | 1.2.Формализованный анализ и оценка программ и моделей программ | 2 | Программные инструменты для “проверки моделей” программ | 32, 33, 34, 35, 36, 37 |
| 6 | 1.2.Формализованный анализ и оценка программ и моделей программ | 2 | Символьное выполнение и абстрактная интерпретация | 38, 39, 40, 41 |
| 7 | 1.3.Формализация процессов обработки данных | 2 | Основы формализации процессов | 42, 43, 44, 45 |
| 8 | 1.3.Формализация процессов обработки данных | 2 | Формальный язык CSP Ч.А.Р. Хоара и его применения | 46, 47, 48, 49, 50, 51 |
| 9 | 1.3.Формализация процессов обработки данных | 2 | Обзор формализмов связанных с языком или основанных на языке CSP | 52, 53, 54, 55 |
| 10 | 1.4.Формальные модели оценки сложности программ | 2 | Оценки предельной сложности вычислений | 56, 57, 58, 59, 60 |
| 11 | 1.4.Формальные модели оценки сложности программ | 2 | Теория сводимости | 61, 62, 63, 64 |
| Итого: | 26 | |||
-
Практические занятия
| № п/п | Раздел дисциплины | Объем, часов | Тема практического занятия | Дидакт. единицы |
| Итого: | ||||
-
Лабораторные работы
| № п/п | Раздел дисциплины | Наименование лабораторной работы | Наименование лаборатории | Объем, часов | Дидакт. единицы |
| 1 | 1.2.Формализованный анализ и оценка программ и моделей программ | Проведение доказательства программы формулизацией переходов от пред-условий к постусловиям | 4 | 15, 16, 23 | |
| 2 | 1.2.Формализованный анализ и оценка программ и моделей программ | Формальная верификация модели программы с помощью верификаторов SPIN, SVM, BLAST | 4 | 26, 27, 32, 33, 34, 35, 36 | |
| 3 | 1.2.Формализованный анализ и оценка программ и моделей программ | Применение формализмов Хоара и Милнера для верификации процессов | 4 | 42, 43, 44, 45, 46, 48, 49, 50, 51, 52, 53 | |
| Итого: | 12 | ||||
-
Типовые задания
| № п/п | Раздел дисциплины | Объем, часов | Наименование типового задания |
| Итого: | |||
-
Курсовые работы и проекты по дисциплине
-
Рубежный контроль
-
Промежуточная аттестация
1. Зачет (8 семестр)
Прикрепленные файлы: Вопросы к зачёту по формальным методам.doc
-
УЧЕБНО-МЕТОДИЧЕСКОЕ И ИНФОРМАЦИОННОЕ ОБЕСПЕЧЕНИЕ ДИСЦИПЛИНЫ
а)основная литература:
1. Карпов Ю. Г. Model Checking. Верификация параллельных и распределенных программных систем. СПб.: БХВ-Петербург. 2009. ISBN 978-5-9775-0404-1
2. Гагарин, А.П. Элементы технологии программирования примерах и упражнениях (электронный конспект), 2013, 70 с.
3. А.М.Миронов Теория процессов http://intsys.msu.ru/staff/mironov/processes.pdf
4. М.Гэри, Д.Джонсон Вычислительные машины и труднорешаемые задачи. - М.: Мир, 1982. - С. 5-63
б)дополнительная литература:
1. Д. Скотт. Теория решеток, типы данных и семантика// Данные в языках программирования. - М.: Мир, 1982. - С. 25-53
2. Д.С.Скотт. Области в денотационной семантике. Перевод Воронкова А.А. Сб. Математическая логика в программировании. Пер. с англ. под ред. М.В.Захарьящева и и Ю.И.Янова. - М.: Мир, 1970. - С.58 - 118
3. Ч.Хоар Взаимодействующие последовательные процессы. – М.: Мир, 1989. – С.261
4. М.Блюм Машинно-независимая теория сложности рекурсивных функций. В сб. Проблемы математической логики под ред. В.А.Козмидиади и А.А.Мучника. - М.: Мир, 1970. - С. 401-422.
5. М.Блюм Об эффективных процедурах для ускоряющих алгоритмов. В сб. Сложность вычислений и алгоритмов под ред. В.А.Козмидиади, А.Н.Маслова, Н.В.Петри. - М.: Мир, 1974. - С. 127-149.
6. Голдблатт Р. Логика времени и вычислимость. М.: Мир, 1993
7. Zohar Manna, Richard Waldinger (Jan 1980). "A Deductive Approach to Program Synthesis". ACM Transactions on Programming Languages and Systems 2: 90–121
8. Х.Барендрегт Ламбда-исчисление. Его синтаксис и семантика. пер. с англ. Г.Е.Минца. М.: Мир, 1985. -606 с.
9. З.Манна Теория неподвтжной точки программ. Пер. С.В.Попова в сб. Кибеонетический сборник. Новая серия. Выпуск 15. М.: Мир, 1978. с. 38 - 100
10.К.А.Гоуд Доказательства как описание вычислений. Перевод Воронкова А.А. Сб. Математическая логика в программировании. Пер. с англ. под ред. М.В.Захарьящева и и Ю.И.Янова. - М.: Мир, 1970. - С.311 - 330
Литература из электронного каталога:
1. Боггс У. Боггс У. UML и Rational Rose . ЛОРИ, 2008. - ЛОРИ, 2008.
2. Блаха М. Блаха М. UML 2.0.Объектно-ориентированное моделирование и разработка. Питер, 2007. - 540 с. - Питер, 2007.
3. Боггс М. Боггс М. UML и Rational Rose 2002. ЛОРИ, 2004. - 509 с. - ЛОРИ, 2004.
в)программное обеспечение, Интернет-ресурсы, электронные библиотечные системы:
верификатор SPIN (открытый продукт)
анализатор моделй NuSMV (открытый продукт)
анализатор моделей BLAST (открытый продукт)
-
МАТЕРИАЛЬНО-ТЕХНИЧЕСКОЕ ОБЕСПЕЧЕНИЕ ДИСЦИПЛИНЫ
1)компьютерный класс, оснащённый операционной средой типа Windows и операционной средой типа Unix (Linux)
Приложение 1
к рабочей программе дисциплины
«Формальные методы в программной инженерии »
Аннотация рабочей программы
Дисциплина Формальные методы в программной инженерии является частью Профессионального цикла дисциплин подготовки студентов по направлению подготовки Программная инженерия. Дисциплина реализуется на 3 факультете «Московского авиационного института (национального исследовательского университета)» кафедрой (кафедрами) 304.
Дисциплина нацелена на формирование следующих компетенций: ПК-2 ,ПК-4 ,ПК-5 ,ПК-6 ,ПК-10 ,ПК-12 ,ПК-23 ,ПК-24 ,ПСК-11.
Содержание дисциплины охватывает круг вопросов, связанных с: формальной верификацией программ на основе алгебраических и логико-математических моделей программ с применением специальных языков и инструментальных программных средств
Преподавание дисциплины предусматривает следующие формы организации учебного процесса: Лекция, мастер-класс, Лабораторная работа.
Программой дисциплины предусмотрены следующие виды контроля: промежуточная аттестация в форме Зачет (8 семестр).
Общая трудоемкость освоения дисциплины составляет 2 зачетных единиц, 72 часов. Программой дисциплины предусмотрены лекционные (26 часов), практические (0 часов), лабораторные (12 часов) занятия и (34 часов) самостоятельной работы студента.
Приложение 2
к рабочей программе дисциплины
«Формальные методы в программной инженерии »
Cодержание учебных занятий
-
Лекции
1.1.1. Сущность, цели и направления формализации технологий программной инженерии (АЗ: 4, СРС: 4)
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
