Распределение курсов «Формальные методы верификации программ» по темам и часам:
Общий учебный час
|
180 час
|
В том числе:
|
Лекция
|
30 час
|
Практика
|
60 час
|
Самостоятельное обучение
|
90 час
|
Форма занятий: лекция (Л)
|
часы
|
|
Введение в формальные методы верификации программ
|
2
|
|
Формализация семантики языков программирования
|
2
|
|
Дедуктивная верификация последовательных программ
|
2
|
|
Инструменты дедуктивной верификации программ
|
2
|
|
Метод индуктивных утверждений
|
2
|
|
Метод фундированных множеств
|
2
|
|
Автоматический синтез инвариантов циклов
|
2
|
|
Автоматическое доказательство условий верификации
|
2
|
|
Спецификация и верификация параллельных программ
|
2
|
|
Инструменты проверки моделей
|
2
|
|
Моделирование программ структурами Крипке
|
2
|
|
Автоматы Бюхи и -регулярные языки
|
2
|
|
Синтез автомата Бюхи по формуле LTL
|
2
|
|
Символическая проверка моделей
|
2
|
|
Использование формальных методов в тестировании
|
2
|
Всего
|
30
|
Форма занятий: Практика (П)
|
часы
|
|
Анализ ошибок в программах и верификации программ
|
4
|
|
Язык программирования while и типы семантики
|
4
|
|
Дедуктивные системы и виды верификации программ
|
4
|
|
Язык ACSL и платформа Frama-C
|
4
|
|
Синтаксис и семантика блок-схем
|
4
|
|
Метод фундированных множеств и метод счетчиков
|
4
|
|
Эвристические методы синтеза инвариантов и абстрактная интерпретация
|
4
|
|
Задача выполнимости, SAT и SMT решатели. Метод резолюций для логики предикатов первого порядка
|
4
|
|
Реагирующие системы, Темпоральная логика LTL, Алгоритм Петерсона взаимного исключения процессов
|
4
|
|
Язык программирования Promela и введение в инструмент Spin
|
4
|
|
Структура Крипке и предикатная абстракция и уточнение абстракции по контрпримерам
|
4
|
|
Теоретико-автоматный подход к проверке моделей и автомат Бюхи
|
4
|
|
Состояния, переходы и алгоритмы автомата Бюхи
|
4
|
|
Символические методы верификации, символическая проверка и двоичные решающие диаграммы
|
4
|
|
Виды тестирования и формальная верификация
|
4
|
|
Всего
|
60
|
Темы для самостоятельная работа
|
часы
|
|
Верификация программ
|
3
|
|
|
Формальная верификация программ
|
3
|
|
|
Проверка модели
|
3
|
|
|
Дедуктивный анализ
|
3
|
|
|
Формальная семантика
|
3
|
|
|
Операционная семантика и аксиоматическая семантика
|
3
|
|
|
Доказательное программирование
|
3
|
|
|
Дедуктивные системы и доказательства. Значимость и полнота дедуктивных систем
|
3
|
|
|
Верификация программ на языке while. Верификация линейных программ. Верификация ациклических программ
|
3
|
|
|
Верификация циклических программ
|
3
|
|
|
Платформа Frama-C
|
3
|
|
|
Модуль Jessie и платформа Why3
|
3
|
|
|
Метод индуктивных утверждений
|
3
|
|
|
Общая схема метода Флойда
|
3
|
|
|
Дедуктивная система для доказательства полной корректности
|
3
|
|
|
Эвристические методы синтеза инвариантов
|
3
|
|
|
Абстрактная интерпретация и примеры упрощенных моделей
|
3
|
|
|
Логика высказываний и SAT-решатели
|
3
|
|
|
Алгоритм DPLL проверки выполнимости
|
3
|
|
|
SMT-решатели
|
3
|
|
|
Комбинирование теорий
|
3
|
|
|
Реагирующие системы
|
3
|
|
|
Темпоральная логика LTL
|
3
|
|
|
Алгоритм Петерсона взаимного исключения процессов
|
3
|
|
|
Доказательство корректности алгоритма Петерсона
|
3
|
|
|
Основные опции SPIN
|
3
|
|
|
Уточнение абстракции по контрпримерам (CEGAR
|
3
|
|
|
Проверка языка, допускаемого автоматом Бюхи, на пустоту
|
3
|
|
|
Общая схема проверки моделей для логики LTL
|
3
|
|
|
Обход графа состояний программы. Абстракция состояний программы
|
3
|
|
|
Всего
|
90
|
|
Стратегия обучения
Курс Формальные методы верификации программ структурирован следующим образом: теория и решение проблем, тест и контрольные работы, а также самостоятельное обучение. На протяжении теоретических занятий преподаватель предоставляет студенту необходимые концепции и понятия по предмету. В практических и лабораторных занятиях учитель объясняет студентам ряд проблем, в которых учащиеся учатся определять элементы, которые важны для решения проблемы. Используется подход, основанный на участии, и общение между студентом и учителем /студентом имеет важное значение в проблемных профессиях.
У студента будут следующие документы:
Видео лекции;
Электронные лекционные материалы;
Презентационные слайды для каждой темы (лекции) курса;
Методические указания для лабораторных работ;
Методические указания для практических работ;
Задания на каждое занятие;
Электронные книги и пособия.
Во время теоретических занятий студенту будут предоставлены необходимые концепции по теме посредством видео лекции. Студентам будут даны инструкции о том, как использовать презентации, учебники, руководства и другие учебные пособия для усиления темы. Чтобы проверить уровень усвоения темы, студенты проходят тестирование после каждой темы. Если студент завершит эти тесты на необходимом уровне, студенту будет разрешено перейти к следующей теме.
Студентам будут предоставлены материалы, презентации, инструкции по решению задач по каждой теме на лабораторных и практических занятиях, а также задания для проверки уровня усвоения темы. Студенты должны будут работать независимо над каждым разделом курса Операционные системы. Переход на следующую тему осуществляется при правильном выполнении задания.
К участию в итоговом контроле допускаются студенты, освоившие все темы лекционных, лабораторных и практических занятий. Студент приходит в вуз в конце семестра и проходит итоговый контроль.
Оценивание студентов
Оценка знаний студентов производится по показателям усвоения учебных материалов в течение семестра и итогового контроля (результаты тестов, заданий и письменной работы).
Во время курса Операционные системы студенты оцениваются по 100-балльной шкале. Из них 50% баллов начисляются за посещаемость, текущие и промежуточные результаты, а 50% баллов - за итоговый контроль. Учащиеся, набравшие менее 30 баллов по текущему и промежуточному баллам, к итоговому контрольному экзамену не допускаются. Считается, что студент, набравший 30 или более баллов на итоговом тесте, освоил предмет.
Текущие, промежуточные и итоговые контрольные баллы распределяются следующим образом:
Список задач
|
%
|
Семестр
|
50
|
Самостоятельные работы (1 шт)
|
5
|
Практические работы (15 шт)
|
15
|
1-й Промежуточные контроль
|
15
|
2-й Промежуточные контроль
|
15
|
Итоговый контроль
|
50
|
Основная литература
|
|
Введение в формальные методы верификации программ. А. С. Камкин, МОСКОВСКИЙ государственный университет имени М. В. ЛОМОНОСОВА.
Introduction to formal methods for program verification: textbook / A. S. Kamkin. – Moscow : MAKS Press, 2018.
|
Рекомендуемая дополнительная литература
|
|
Formal verification of systems. Alessandro Abate, 2017
|
Электронные источники:
|
|
http://frama-c.com/jessie.html
https://moodle.ubtuit.uz/
http://frama-c.com/
http://javapathfinder.sourceforge.net/
http://spinroot.com/spin/Man/promela.html
http://vlsi.colorado.edu/~fabio/CUDD/
http://krakatoa.lri.fr/
http://spinroot.com/
http://why3.lri.fr/
|
Do'stlaringiz bilan baham: |
