Математические методы верификации схем и программ — различия между версиями

Материал из Кафедра математической кибернетики
Перейти к: навигация, поиск
м
Строка 1: Строка 1:
 +
= Общая информация =
 +
 
Обязательный курс для магистров 618 и 621 группы 11 семестра обучения.  
 
Обязательный курс для магистров 618 и 621 группы 11 семестра обучения.  
  
 
Курс читают  
 
Курс читают  
  
профессор [[Захаров Владимир Анатольевич|В. А. Захаров]]
+
* профессор [[Захаров Владимир Анатольевич|В. А. Захаров]]
 
+
* младший научный сотрудник [[Подымов Владислав Васильевич|В. В. Подымов]].
младший научный сотрудник [[Подымов Владислав Васильевич|В. В. Подымов]].
+
  
 
Лекционная нагрузка — 32 ч., семинары и практические занятия— 16 ч.
 
Лекционная нагрузка — 32 ч., семинары и практические занятия— 16 ч.
  
== Программа ==
+
= Программа =
  
 
#Задача верификации аппаратуры и программного обеспечения. Зачем нужна формальная верификация программ? Основные подходы к задаче формальной верификации. Принципы верификации моделей программ. Исторические сведения. Достижения методов формальной верификации программ. Алгоритмические и комбинаторные трудности применения метода верификации моделей программ. '''[[Media: Lecture_Verification_1.pdf| Лекция 1.]]'''
 
#Задача верификации аппаратуры и программного обеспечения. Зачем нужна формальная верификация программ? Основные подходы к задаче формальной верификации. Принципы верификации моделей программ. Исторические сведения. Достижения методов формальной верификации программ. Алгоритмические и комбинаторные трудности применения метода верификации моделей программ. '''[[Media: Lecture_Verification_1.pdf| Лекция 1.]]'''
Строка 19: Строка 20:
 
#Табличная верификация моделей для PLTL. Автоматы Бюхи: их свойства и обобщения. Трансляция формул PLTL в автоматы Бюхи. Сведение задачи проверки выполнимости формул PLTL к проблеме пустоты для автоматов Бюхи. Алгоритм двойного поиска в глубину с возвратом (DDFS) для проверки пустоты автоматов Бюхи. '''[[Media: Lecture_Verification_7.pdf| Лекция 7.]]'''
 
#Табличная верификация моделей для PLTL. Автоматы Бюхи: их свойства и обобщения. Трансляция формул PLTL в автоматы Бюхи. Сведение задачи проверки выполнимости формул PLTL к проблеме пустоты для автоматов Бюхи. Алгоритм двойного поиска в глубину с возвратом (DDFS) для проверки пустоты автоматов Бюхи. '''[[Media: Lecture_Verification_7.pdf| Лекция 7.]]'''
  
== Литература ==
+
= Материалы семинаров =
 +
 
 +
'''[[Media: Seminar_Verification_1.pdf| Семинар 1.]]''' Доказательство корректности императивных программ с помощью логики Хоара.
 +
 
 +
'''Домашнее задание 1:''' см. семинар 1; решение высылать на почту valdus@yandex.ru в любом нерукописном цифровом виде (.txt, .doc, TeX, ...); крайний срок сдачи: '''27 сентября, 23:59'''; поощрение за сделанное домашнее задание: '''освобождение от задачи на тему логики Хоара'''.
 +
 
 +
= Литература =
  
 
#Э.М. Кларк, О. Грамберг, Д. Пелед. Верификация моделей программ: Model Checking. Изд-во МЦНМО, 2002.
 
#Э.М. Кларк, О. Грамберг, Д. Пелед. Верификация моделей программ: Model Checking. Изд-во МЦНМО, 2002.

Версия 12:26, 14 сентября 2016

Общая информация

Обязательный курс для магистров 618 и 621 группы 11 семестра обучения.

Курс читают

Лекционная нагрузка — 32 ч., семинары и практические занятия— 16 ч.

Программа

  1. Задача верификации аппаратуры и программного обеспечения. Зачем нужна формальная верификация программ? Основные подходы к задаче формальной верификации. Принципы верификации моделей программ. Исторические сведения. Достижения методов формальной верификации программ. Алгоритмические и комбинаторные трудности применения метода верификации моделей программ. Лекция 1.
  2. Общие принципы дедуктивной верификации программ. Операционная семантика императивных программ. Формальная постановка задачи верификации программ. Логика Хоара: правила вывода и свойства. Автоматизация проверки правильности программ. Лекция 2.
  3. Моделирование схем. Системы переходов - модели Крипке. Представление систем переходов формулами логики предикатов первого порядка. Синхронные и асинхронные схемы. Степень детализации представления. Трансляция описаний программ и схем в модели Крипке. Лекция 3.
  4. Темпоральная логика деревьев вычислений CTL. Синтаксис и семантика CTL. Примеры спецификаций моделей в терминах формул CTL. Темпоральная логика линейного времени PLTL. Синтаксис и семантика PLTL. Свойства живости и безопасности. Ограничения справедливости. Задача верификации моделей (model-checking). Лекция 4.
  5. Табличный алгоритм верификации моделей для CTL. Обоснование корректности и сложности табличного алгоритма верификации моделей. Проблема “комбинаторного взрыва”. Символьные средства описания моделей. Двоичные разрешающие диаграммы (BDD). Алгоритм редукции BDD к каноническому виду (OBDD). Выполнение операций над OBDD: унарные и бинарные булевы операции, квантификация, проверка выполнимости, подсчет числа единиц. Общие представления о сложности в классе OBDD. Лекция 5.
  6. Представления неподвижной точки в CTL. Алгоритм символьной верификации моделей в CTL. Особенности реализации алгоритма: учет ограничений справедливости, расщепленные отношения переходов, рекомбинация произведений. Лекция 6.
  7. Табличная верификация моделей для PLTL. Автоматы Бюхи: их свойства и обобщения. Трансляция формул PLTL в автоматы Бюхи. Сведение задачи проверки выполнимости формул PLTL к проблеме пустоты для автоматов Бюхи. Алгоритм двойного поиска в глубину с возвратом (DDFS) для проверки пустоты автоматов Бюхи. Лекция 7.

Материалы семинаров

Семинар 1. Доказательство корректности императивных программ с помощью логики Хоара.

Домашнее задание 1: см. семинар 1; решение высылать на почту valdus@yandex.ru в любом нерукописном цифровом виде (.txt, .doc, TeX, ...); крайний срок сдачи: 27 сентября, 23:59; поощрение за сделанное домашнее задание: освобождение от задачи на тему логики Хоара.

Литература

  1. Э.М. Кларк, О. Грамберг, Д. Пелед. Верификация моделей программ: Model Checking. Изд-во МЦНМО, 2002.
  2. Ю.Г. Карпов. Model Checking: верификация параллельных и распределенных программных систем. Изд-во БХВ-Петербург, 2010.
  3. K. R. Apt, E.-R. Olderog. Verification of sequential and concurrent programs, Springer, 1997.
  4. B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, P. Schnoebelen. Systems and Software Verification: Model-Checking Techniques and Tools. Springer, 2001.
  5. Baier C., Katoen J.-P. Principles of model checking, MIT Press, 2008.