Версия 20:16, 10 ноября 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 к проблеме пустоты для автоматов Бюхи. Лекция 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. Доказательство корректности императивных программ с помощью логики Хоара.

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

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

Семинар 4. Обзор средства NuSMV: описание параллельной композиции автоматов, проверка CTL-формул.

Семинар 5-6. NuSMV: практические задания по проверке CTL-спецификаций.

Семинар 7. Обзор средства SPIN: синтаксис, трансляция базовых конструкций в модели Крипке.

Инструкция по работе со средством SPIN.

Домашние задания

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

Домашнее задание 1: логика Хоара

Домашнее задание сформулировано в слайдах семинара 1.

Решение должно быть нерукописным (.txt, .doc, TeX-pdf, ...).

Крайний срок сдачи: 27 сентября, 23:59.

Поощрение за сделанное домашнее задание: освобождение от задачи на тему логики Хоара.

Домашнее задание 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: формализация систем и свойств, алгоритмы проверки CTL-формул

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

Домашнее задание 4, сложное: символьный алгоритм проверки CTL-формул

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

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

• задание можно выполнять как в одиночку, так и в паре
• написать письмо с любым содержанием и заголовком
  • "[Ver 2016 nusmv] Фамилия И.О.", если задание выполняется в одиночку
  • "[Ver 2016 nusmv] Фамилия И.О. Фамилия И.О.", если задание выполняется в паре
• в ответ будут присланы описание системы и требований к ней
• задача: описать систему и требования в формате NuSMV так, чтобы можно было проверить требования обычным для NuSMV образом
• необходимо выслать ответом на присланное письмо файл с расширением .smv, содержащий описание системы и требований в формате NuSMV
• если есть предпочтения: из какой области хотелось бы видеть описание системы - то эти предпочтения можно выразить в тексте первого письма
  • если предпочтения разумны, то они могут быть учтены
  • например, на семинаре 5 было озвучено несколько таких областей: параллельно работающие программы, схемы, игры/головоломки, системы общего вида
• крайний срок сдачи: 15.11.2016, 23:59
• поощрение за выполненное домашнее задание: необходимо для допуска к экзамену
• наказание за невыполненное домашнее задание: сдача этого задания перед экзаменом в более сжатые сроки
• обратите внимание на то, что присланное решение будет сразу принято либо не принято, без итераций с исправлением ошибок
  • рекомендуется задействовать все средства, позволяющие убедиться, что система и требования описаны правильно
  • если задание выполняется в паре, рекомендуется каждому участнику проверить правильность итогового .smv-файла

Литература

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.