Министерство по развитию информационных технологий и коммуникаций республики узбекистан ургенчский филиал ташкентского университета информационных технологий имени мухаммада аль-хоразмий


Распределение курсов «Формальные методы верификации программ» по темам и часам


Download 89.41 Kb.
bet3/3
Sana21.02.2023
Hajmi89.41 Kb.
#1216625
1   2   3
Bog'liq
Sillabus ВФМВП рус Abdullayev Anvar

Распределение курсов «Формальные методы верификации программ» по темам и часам:

Общий учебный час

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


Основная литература




  1. Введение в формальные методы верификации программ. А. С. Камкин, МОСКОВСКИЙ государственный университет имени М. В. ЛОМОНОСОВА.

  2. Introduction to formal methods for program verification: textbook / A. S. Kamkin. – Moscow : MAKS Press, 2018.

Рекомендуемая дополнительная литература




  1. Formal verification of systems. Alessandro Abate, 2017

Электронные источники:




  1. http://frama-c.com/jessie.html

  2. https://moodle.ubtuit.uz/

  3. http://frama-c.com/

  4. http://javapathfinder.sourceforge.net/

  5. http://spinroot.com/spin/Man/promela.html

  6. http://vlsi.colorado.edu/~fabio/CUDD/

  7. http://krakatoa.lri.fr/

  8. http://spinroot.com/

  9. http://why3.lri.fr/

Download 89.41 Kb.

Do'stlaringiz bilan baham:
1   2   3




Ma'lumotlar bazasi mualliflik huquqi bilan himoyalangan ©fayllar.org 2024
ma'muriyatiga murojaat qiling