Математические методы верификации схем и программ

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

Обязательный курс для магистров 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. Безопасность, живость, справедливость.

Семинар 3. Табличный и символьный алгоритмы проверки CTL-формул на моделях Крипке. ROBDD.

Домашнее задание 2, обязательное:

• (прежде всего) поставить NuSMV
• (чуть позже, но тоже надо) поставить Spin
• (ещё позже, но тоже надо) поставить UPPAAL (лучше версию 4.0, но можно и последнюю)
• настоятельно рекомендуется всё это поставить в Linux (с Windows у студентов постоянно возникают странные проблемы, а в Linux всё работает - проверено)
• проверить, что всё это работает:
  • в выводе "./NuSMV" есть строки, утверждающие, что
    • подключены CUDD и MiniSat, либо нет строк о том, что что-то надо подключить
    • входной файл не подан и работа завершена
  • "./spin -a <папка с примерами spin>/LTL/bakery.pml" успешно завершает работу без вывода
  • "./uppaal" загружает графический интерфейс и для какого-нибудь примера при нажатии на кнопку Check вкладки Verifier при каком-нибудь выделенном свойстве завершает вывод словами Property is satisfied или Property is not satisfied
• Организовать хотя бы один ноутбук на двоих (если совсем не выходит, то на троих) с поставленным NuSMV на занятии 21.10.2016

Домашнее задание 3, по желанию:

• написать письмо с любым содержанием и заголовком "[Ver 2016 hw2] Фамилия И.О."
• в ответ будут присланы описание системы и требований к этой системе
• задача: поработать в качестве табличного или символьного алгоритма верификации CTL-формул и донести результат в любом виде
  • табличный алгоритм:
    • нарисовать модель Крипке
    • записать требования в виде CTL-формул
    • описать шаги работы алгоритма настолько (не)строго, чтобы можно было без чрезмерных усилий строго восстановить каждый шаг работы
  • символьный алгоритм:
    • записать набор формул для модели Крипке
    • записать требования в виде CTL-формул
    • описать шаги работы алгоритма (включающее BDD, QBF или аналогичную формальную запись) настолько (не)строго, чтобы можно было без чрезмерных усилий строго восстановить каждый шаг работы

Домашнее задание 4, по желанию, сложное:

• этим заданием покрывается домашнее задание 3
• привести описание символьного алгоритма верификации CTL-формул, работающего в условиях справедливости для CTL
  • можно написать псевдокод с пояснениями
  • можно описать на естественном языке, но так, чтобы можно было без чрезмерных усилий строго восстановить каждый шаг работы алгоритма
  • можно написать программу
  • ...
• привести пример работы алгоритма, иллюстрирующий его отличие от "несправедливого" символьного алгоритма

Семинар 4. Обзор средства NuSMV: описание параллельной композиции автоматов, проверка 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.