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

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

Версия 13:26, 9 сентября 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. Э.М. Кларк, О. Грамберг, Д. Пелед. Верификация моделей программ: 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.