rpd000012698 (1010444), страница 3

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 3)

Тип лекции: Информационная лекция

Форма организации: Лекция, мастер-класс

1.1.2. Логико-математические и алгебраические основы “формальных методов” (АЗ: 4, СРС: 4)

Тип лекции: Информационная лекция

Форма организации: Лекция, мастер-класс

1.2.1. Верификация последовательных программ (АЗ: 2, СРС: 2)

Тип лекции: Информационная лекция

Форма организации: Лекция, мастер-класс

1.2.2. Формальная верификация путём “проверки моделей” (model checking)

(АЗ: 2, СРС: 2)

Тип лекции: Информационная лекция

Форма организации: Лекция, мастер-класс

1.2.3. Программные инструменты для “проверки моделей” программ (АЗ: 2, СРС: 2)

Тип лекции: Информационная лекция

Форма организации: Лекция, мастер-класс

1.2.4. Символьное выполнение и абстрактная интерпретация (АЗ: 2, СРС: 2)

Тип лекции: Информационная лекция

Форма организации: Лекция, мастер-класс

1.3.1. Основы формализации процессов (АЗ: 2, СРС: 2)

Тип лекции: Информационная лекция

Форма организации: Лекция, мастер-класс

1.3.2. Формальный язык CSP Ч.А.Р. Хоара и его применения (АЗ: 2, СРС: 2)

Тип лекции: Информационная лекция

Форма организации: Лекция, мастер-класс

1.3.3. Обзор формализмов связанных с языком или основанных на языке CSP (АЗ: 2, СРС: 2)

Тип лекции: Информационная лекция

Форма организации: Лекция, мастер-класс

1.4.1. Оценки предельной сложности вычислений

(АЗ: 2, СРС: 2)

Тип лекции: Информационная лекция

Форма организации: Лекция, мастер-класс

1.4.2. Теория сводимости (АЗ: 2, СРС: 2)

Тип лекции: Информационная лекция

Форма организации: Лекция, мастер-класс

1. Практические занятия

1. Лабораторные работы

1.2.1. Проведение доказательства программы формулизацией переходов от пред-условий к постусловиям (АЗ: 4, СРС: 4)

Форма организации: Лабораторная работа

1.2.2. Формальная верификация модели программы с помощью верификаторов SPIN, SVM, BLAST (АЗ: 4, СРС: 2)

Форма организации: Лабораторная работа

1.2.3. Применение формализмов Хоара и Милнера для верификации процессов (АЗ: 4, СРС: 2)

Форма организации: Лабораторная работа

1. Типовые задания

Приложение 3
к рабочей программе дисциплины
«Формальные методы в программной инженерии »

Прикрепленные файлы

Вопросы к зачёту по формальным методам.doc

ВОПРОСЫ

к зачёту по дисциплине “Формальные методы в программной инженерии”

1. Эксперимент и логический вывод в обосновании суждений об информационных процессах и программах.

2. Типовые ситуации применения приёмов формализации, абстрагирования и конкретизации в ходе разработки компьютерных программ.

3. Классификация подходов к семантике языков программирования и спецификаций (структурная, денотационная и другие разновидности семантики).

4. Метод денотационного моделирования VDM.

5. Язык параметризованных схем Z, его структура и характер применения.

6. Алгебраическая спецификация абстрактных типов данных.

7. Подходы к формальному синтезу программ.

8. Доказательство свойств программ путём формализации предусловий, пост- условий и переходов между ними.

9. Аксиоматика Флойда-Хоара.

10. Логика PDL.

11. Язык PROMELA и его применение для верификации моделей процессов.

12. Линейная временная логика LTL и её применение для верификации.

13. Ветвящаяся временная логика CTL и её применение для верификации.

14. Диаграммы UML и F-логика.

15. Программные инструменты для “проверки моделей” программ.

16. Концепция верификации программ путём “символьного выполнения”.

17. Концепция верификации программ путём “абстрактной интерпретации”.

18. Определение понятия процесса и подходы к его формализации.

19. Примитивы и алгебраические операторы языка CSP.

20. Денотационные семантические модели языка CSP.

21. Исчисление процессов CCS Р. Милнера.

22. Языки LOTOS и Circus и их применение при проектировании программ.

23. Подходы к формализации сложности вычислений.

24. Понятие сигнализирующей функции и аксиомы Блюма для сигнализирующих функций.

25. Теорема о нижней грани и теоремы о сжимании.

26. Решение массовой задачи недетерминированной машиной Тьюринга.

27. Понятие полиномиальной сводимости, определение класса NP-полных задач.

28. Примеры NP-полных задач

Версия: AAAAAAUQsrM Код: 000012698

Характеристики

Список файлов учебной работы