rpd000012698 (1010444)
Текст из файла
Министерство образования и науки Российской Федерации
Федеральное государственное бюджетное образовательное учреждение высшего профессионального образования
Московский авиационный институт
(национальный исследовательский университет)
УТВЕРЖДАЮ
Проректор по учебной работе
______________Куприков М.Ю.
“____“ ___________20__
РАБОЧАЯ ПРОГРАММА ДИСЦИПЛИНЫ (000012698)
Формальные методы в программной инженерии
(указывается наименование дисциплины по учебному плану)
| Направление подготовки | Программная инженерия | |||||
| Квалификация (степень) выпускника | Бакалавр | |||||
| Профиль подготовки | Программно-информационные системы | |||||
| Форма обучения | очная | |||||
| (очная, очно-заочная и др.) | ||||||
| Выпускающая кафедра | 304 | |||||
| Обеспечивающая кафедра | 304 | |||||
| Кафедра-разработчик рабочей программы | 304 | |||||
| Семестр | Трудоем-кость, час. | Лек-ций, час. | Практич. занятий, час. | Лаборат. работ, час. | СРС, час. | Экзаменов, час. | Форма промежуточного контроля |
| 8 | 72 | 26 | 0 | 12 | 34 | 0 | Зч |
| Итого | 72 | 26 | 0 | 12 | 34 | 0 |
Москва
2011
РАБОЧАЯ ПРОГРАММА ДИСЦИПЛИНЫ
Разделы рабочей программы
-
Цели освоения дисциплины
-
Структура и содержание дисциплины
-
Учебно-методическое и информационное обеспечение дисциплины
-
Материально-техническое обеспечение дисциплины
Приложения к рабочей программе дисциплины
Приложение 1. Аннотация рабочей программы
Приложение 2. Cодержание учебных занятий
Приложение 3. Прикрепленные файлы
Программа составлена в соответствии с требованиями ФГОС ВПО по направлению подготовки 231000 Программная инженерия
Авторы программы:
| Гагарин А.П. | _________________________ |
| Заведующий обеспечивающей кафедрой 304 | _________________________ |
Программа одобрена:
| Заведующий выпускающей кафедрой 304 _________________________ | Декан выпускающего факультета 3 _________________________ |
-
ЦЕЛИ ОСВОЕНИЯ ДИСЦИПЛИНЫ
Целью освоения дисциплины Формальные методы в программной инженерии является достижение следующих результатов образования (РО):
| N | Шифр | Результат освоения |
| 1 | Способность следить за развитием формальных методов верификации программ применять их в своей практике | |
| 2 | Возможность участвовать в развитии формальных методов верификации программ | |
| 3 | Умение определять границы применимости методов формальной верификации программ | |
| 4 | Умение пользоваться методами формальной верификации программ |
Перечисленные РО являются основой для формирования следующих компетенций: (в соответствии с ФГОС ВПО и требованиями к результатам освоения основной образовательной программы (ООП))
| N | Шифр | Компетенция |
| 1 | ПК-2 | Способность к формализации в своей предметной области с учетом ограничений используемых методов исследования |
| 2 | ПК-4 | Готовность обосновать принимаемые проектные решения, осуществлять постановку и выполнение экспериментов по проверке их корректности и эффективности |
| 3 | ПК-5 | Умение готовить презентации, оформлять научно-технические отчеты по результатам выполненной работы, публиковать результаты исследований в виде статей и докладов на научно-технических конференциях |
| 4 | ПК-6 | Способность формализовать предметную область программного проекта и разработать спецификации для компонентов программного продукта |
| 5 | ПК-10 | Умение применять основы информатики и программирования к проектированию, конструированию и тестированию программных продуктов |
| 6 | ПК-12 | Навыки моделирования, анализа и использования формальных методов конструирования программного обеспечения |
| 7 | ПК-23 | Понимание методов управления процессами разработки требований, оценки рисков, приобретения, проектирования, конструирования, тестирования, эволюции и сопровождения |
| 8 | ПК-24 | Понимание основ групповой динамики, психологии и профессионального поведения, специфичных для программной инженерии |
| 9 | ПСК-11 | Способность моделировать и проектировать архитектуру реконфигурируемого модульного программного обеспечения, знание формальных методов, шаблонов и языков разработки спецификаций и архитектуры, основ системного программирования |
| 10 | Понимание основных подходов к построению алгебраических и логико-математических моделей программ | |
| 11 | Умение выражать в формальных моделях и доказывать утверждения о свойствах моделируемых программ | |
| 12 | Умение верифицировать программы с помощью современных инструментальных программных инструментов |
-
СТРУКТУРА И СОДЕРЖАНИЕ ДИСЦИПЛИНЫ
Общая трудоемкость дисциплины составляет 2 зачетных(ые) единиц(ы), 72 часа(ов).
| Модуль | Раздел | Лекции | Практич. занятия | Лаборат. работы | СРС | Всего часов | Всего с экзаменами и курсовыми |
| "Формальные методы" - разновидность технологий программной инженерии | Введение в дисциплину | 8 | 0 | 0 | 8 | 16 | 72 |
| Формализованный анализ и оценка программ и моделей программ | 8 | 0 | 12 | 16 | 36 | ||
| Формализация процессов обработки данных | 6 | 0 | 0 | 6 | 12 | ||
| Формальные модели оценки сложности программ | 4 | 0 | 0 | 4 | 8 | ||
| Всего | 26 | 0 | 12 | 34 | 72 | 72 | |
-
Содержание (дидактика) дисциплины
В разделе приводится полный перечень дидактических единиц, подлежащих усвоению при изучении данной дисциплины.
- 1. Информационные процессы, алгоритмы и компьютерные программы как предмет разработки и оценки их корректности, сложности, эффективности
- 2. Эксперимент и логический вывод в обосновании суждений об информационных процессах и программах
- 3. Градации строгости логического вывода
- 4. Формализация как представление текста в знаковых системах (языках, нотациях), которые обеспечивают определённый (желательный) уровень строгости
- 5. Формализация и абстракция как условие автоматической обработки программных текстов
- 6. Типовые ситуации применения приёмов формализации, абстрагирования и конкретизации в ходе разработки компьютерных программ
- 7. Влияние формализации на понятность программных текстов
- 8. Проблема смысла (семантики) программ, их спецификаций и вычислений
- 9. Прикладное значение формализации семантики языков программирования
- 10. Классификация подходов к семантике языков программирования и спецификаций (структурная, денотационная и другие разновидности семантики)
- 11. Теория доменов Д.Скотта
- 12. Метод денотационного моделирования VDM и язык параметризованных схем Z
- 13. Алгебраическая спецификация абстрактных типов данных
- 14. Теория неподвижной точки программ
- 15. Формальная верификация – логический вывод, удостоверяющий корректность программы или её модели
- 16. Логическая выводимость и истинность суждений
Характеристики
Тип файла документ
Документы такого типа открываются такими программами, как Microsoft Office Word на компьютерах Windows, Apple Pages на компьютерах Mac, Open Office - бесплатная альтернатива на различных платформах, в том числе Linux. Наиболее простым и современным решением будут Google документы, так как открываются онлайн без скачивания прямо в браузере на любой платформе. Существуют российские качественные аналоги, например от Яндекса.
Будьте внимательны на мобильных устройствах, так как там используются упрощённый функционал даже в официальном приложении от Microsoft, поэтому для просмотра скачивайте PDF-версию. А если нужно редактировать файл, то используйте оригинальный файл.
Файлы такого типа обычно разбиты на страницы, а текст может быть форматированным (жирный, курсив, выбор шрифта, таблицы и т.п.), а также в него можно добавлять изображения. Формат идеально подходит для рефератов, докладов и РПЗ курсовых проектов, которые необходимо распечатать. Кстати перед печатью также сохраняйте файл в PDF, так как принтер может начудить со шрифтами.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
