Версия 11:21, 6 октября 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.
8. Особенности параллельных вычислений асинхронных распределенных систем. Независимость действий. Проскальзывающие действия. Достаточные множества переходов и их свойства. Вычисление достаточных множеств переходов. Статическая и динамическая редукция частичных порядков на основе достаточных множеств переходов. Лекция 8.
9. Отношения бисимуляционной эквивалентности (бисимуляции) и симуляционного квазипорядка (симуляции) на моделях Крипке. Равновыполнимость темпоральных формул на бисимуляционно эквивалентных моделях Крипке. Вычисление классов бисимуляционной эквивалентности на конечных моделях Крипке. Упрощение моделей Крипке при помощи отношений симуляции и и бисимуляции. Редукция моделей Крипке по конусу влияния. Абстракции данных при построении моделей Крипке. Лекция 9.
10. Временные автоматы как формальные модели распределенных систем реального времени. Вычисления временных автоматов. Примеры использования временных автоматов для моделирования встроенных систем. Зеноновские вычисления. Синтаксис и семантика Timed CTL. Примеры формальных спецификаций поведения встроенных систем при помощи TCTL. Лекция 10.
11. Задача верификации моделей программ реального времени. Отношение эквивалентности часов и регионы. Регионные системы переходов. Оценка числа регионов. Сведение задачи верификации временных автоматов относительно TCTL к задаче верификации моделей Крипке относительно CTL. Лекция 11.
12. Верификация моделей программ для вычислений ограниченной длины (bounded model checking, BMC). Сведение задачи BMC к задаче проверки выполнимости булевых формул (SAT). Применение автоматических средств решения задачи SAT для решения задачи BMC. Лекция 12.

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

Любые вопросы по темам семинарских занятий можно высылать на почту valdus@yandex.ru.

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

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

Семинар 2. Модели Крипке. LTL, CTL. Безопасность, живость, справедливость.

Литература

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.