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

Материал из Кафедра математической кибернетики
Перейти к: навигация, поиск
 
(не показаны 149 промежуточные версии 3 участников)
Строка 1: Строка 1:
−
Обязательный курс для магистров 618 и 621 группы 11 семестра обучения.  
+
[[Категория:Спецкурсы кафедры МК]]
 +
[[Категория:Лекционные курсы кафедры МК]]
 +
[[Категория:Магистерская программа Дискретные управляющие системы и их приложения]]
 +
''Актуальность информации: осенний семестр 2024/2025 учебного года.''
  
−
Курс читают
+
Обязательный курс для магистров групп 618мк_дса, 618мк_дус и 621асвк 3 семестра магистратуры (группа 621асвк - "Методы верификации программ").
 +
Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].
  
−
профессор [[Захаров Владимир Анатольевич|В. А. Захаров]]
+
= Лекции =
  
−
младший научный сотрудник [[Подымов Владислав Васильевич|В. В. Подымов]].
+
[[Media: Verif_VP_01.pdf|Блок 1]] (вводный). Что такое и зачем нужна формальная верификация.
  
−
Лекционная нагрузка — 32 ч., семинары и практические занятия— 16 ч.
+
[[Media: Verif_VP_02.pdf|Блок 2.]] Логика предикатов (напоминание).
  
−
== Программа ==
+
[[Media: Verif_VP_03.pdf|Блок 3.]] Общие принципы дедуктивной верификации программ. Модельные императивные программы: синтаксис, операционная семантика.
  
−
<h4>Часть 1. Математические модели.</h4>
+
[[Media: Verif_VP_04.pdf|Блок 4.]] Дедуктивная верификация программ: постановка задачи, логика Хоара.
  
−
#Характерные особенности и примеры распределенных систем компьютерные сети, локальные и глобальные сети, многопроцессорные компьютеры). Архитектура распределенных систем. Стандарт ISO Open System Interconnection. Алгоритмические проблемы организации вычислений распределенных систем. Особенности распределенных алгоритмов. '''[[Media: DistrAlg_1.pdf| Лекция 1.]]'''
+
[[Media: Verif_VP_05.pdf|Блок 5.]] Дедуктивная верификация программ: аннотированные программы.
−
#Математическая модель распределенных систем. Системы переходов. Синхронный и асинхронный обмен сообщениями. Зависимые и независимые события. Причинно-следственный порядок событий. Эквивалентность выполнений. Вычисления. Логические часы. Топологии распределенных систем. '''[[Media: DistrAlg_2.pdf| Лекция 2.]]'''
+
−
#:
+
−
#:<h4>Часть 2. Коммуникационные протоколы.</h4>
+
−
#:
+
−
#Коммуникационные протоколы. Ошибки, возникающие при передаче сообщений. Задача надежного обмена сообщениями. Симметричные протокол раздвижного окна: устройство протокола и обоснование его корректности. Протокол альтернирующего бита. '''[[Media: DistrAlg_3.pdf| Лекция 3.]]'''
+
−
#Коммуникационный протокол с таймером: устройство и обоснование корректности. '''[[Media: DistrAlg_4.pdf| Лекция 4.]]'''
+
−
#Задача маршрутизации. Алгоритмы построения кратчайших путей в графе. Алгоритм Флойда-Уоршалла. Алгоритм Туэга. Алгоритм Мерлина-Сигала. Алгоритм Чанди-Мизры. '''[[Media: DistrAlg_5.pdf| Лекция 5.]]''' Алгоритм Netchange. '''[[Media: DistrAlg_6.pdf| Лекция 6.]]'''
+
−
#:
+
−
#:<h4>Часть 3. Распределенные алгоритмы.</h4>
+
−
#:
+
−
#Волновые алгоритмы: определение, основные свойства, область применения. Древесный алгоритм. Алгоритм эха. '''[[Media: DistrAlg_7.pdf| Лекция 7.]]''' Фазовый алгоритм. Алгоритм Финна. Алгоритмы обхода. Распределенный обход в глубину. Алгоритмы обхода Авербаха и Сидон. '''[[Media: DistrAlg_8.pdf| Лекция 8.]]'''
+
−
#Задача избрания лидера. Избрание лидера на кольцах: алгоритм Ченя-Робертса, оптимальный алгоритм Патерсона –Долева-Клейва-Роде. '''[[Media: DistrAlg_9.pdf| Лекция 9.]]''' Избрание лидера в произвольных сетях: алгоритм Галладжера-Хамблета-Спиры, алгоритм Кораха-Каттена-Морана. '''[[Media: DistrAlg_10.pdf| Лекция 10.]]'''
+
−
#Задача обнаружения завершения вычисления. Алгоритм Дейкстры-Шолтена. Алгоритм Шави-Франчеза. Алгоритм Сафры. Алгоритм возвращения кредитов. Алгоритм Раны. '''[[Media: DistrAlg_11.pdf| Лекция 11.]]'''
+
−
#Задача сохранения моментального состояния. Алгоритм Чанди-Лампорта. Алгоритм Лаи-Янга. Применение алгоритмов обнаружения моментальной разметки и завершения вычислений для выявления блокировки вычислений. '''[[Media: DistrAlg_12.pdf| Лекция 12.]]'''
+
−
#:
+
−
#:<h4>Часть 4. Вопросы надежности распределенных алгоритмов.</h4>
+
−
#:
+
−
#Задача обеспечения отказоустойчивости распределенных систем. Невозможность построения робастных асинхронных систем. Синхронные робастные алгоритмы принятия решения. Использование криптографических примитивов для повышения отказоустойчивости.
+
−
#Стабилизирующиеся алгоритмы. Пример Дейкстры. Общие принципы построения стабилизирующихся алгоритмов.
+
  
−
== Литература ==
+
[[Media: Verif_VP_06.pdf|Блок 6.]] Дедуктивная верификация программ: возможности автоматизации, слабейшее предусловие.
  
−
#G. Tel. Introduction to Distributed Algorithms. Cambridge University Press. 2000. (русск. пер. Ж. Тель. Введение в распределенные алгоритмы, изд-во МЦНМО, 2009 г., 616 с.)
+
[[Media: Verif_VP_07.pdf|Блок 7.]] Общая схема метода model checking.
  
−
[[Категория:Лекционные курсы кафедры МК]]
+
[[Media: Verif_VP_08.pdf|Блок 8.]] Модели Крипке.
 +
 
 +
[[Media: Verif_VP_09.pdf|Блок 9.]] Особенности моделирования систем.
 +
 
 +
[[Media: Verif_VP_10.pdf|Блок 10.]] Пара слов о последовательностях.
 +
 
 +
[[Media: Verif_VP_11.pdf|Блок 11.]] Свойства трасс. Безопасность и живость.
 +
 
 +
[[Media: Verif_VP_12.pdf|Блок 12.]] Логика линейного времени (LTL). Постановка задачи верификации моделей Крипке относительно LTL.
 +
 
 +
[[Media: Verif_VP_13.pdf|Блок 13.]] Размеченные системы переходов. Справедливость для систем переходов. Справедливость в LTL.
 +
 
 +
[[Media: Verif_VP_14.pdf|Блок 14.]] Автоматный алгоритм model checking для LTL: общая схема.
 +
 
 +
[[Media: Verif_VP_15.pdf|Блок 15.]] Автоматы Бюхи. Обобщённые автоматы Бюхи.
 +
 
 +
[[Media: Verif_VP_16.pdf|Блок 16.]] Пересечение автоматов Бюхи.
 +
 
 +
[[Media: Verif_VP_17.pdf|Блок 17.]]  Проверка пустоты автомата Бюхи.
 +
 
 +
[[Media: Verif_VP_18.pdf|Блок 18.]] Автоматы Бюхи для моделей Крипке
 +
 
 +
[[Media: Verif_VP_19.pdf|Блок 19.]] Автоматы Бюхи для ltl-формул.
 +
 
 +
[[Media: Verif_VP_20.pdf|Блок 20.]] Автоматный алгоритм model checking для LTL: уточнённая схема.
 +
 
 +
[[Media: Verif_VP_21.pdf|Блок 21.]] Логика деревьев вычислений (CTL). Постановка задачи верификации моделей Крипке относительно CTL.
 +
 
 +
[[Media: Verif_VP_22.pdf|Блок 22.]] Базовый алгоритм model checking для CTL.
 +
 
 +
[[Media: Verif_VP_23.pdf|Блок 23.]] Справедливость и CTL.
 +
 
 +
[[Media: Verif_VP_24.pdf|Блок 24.]] Символьные представления моделей.
 +
 
 +
[[Media: Verif_VP_25.pdf|Блок 25.]] Двоичные решающие диаграммы: BDD, OBDD, ROBDD.
 +
 
 +
[[Media: Verif_VP_26.pdf|Блок 26.]] Символьный алгоритм model checking для CTL (начало).
 +
 
 +
[[Media: Verif_VP_27.pdf|Блок 27.]] Преобразователи предикатов и их неподвижные точки.
 +
 
 +
[[Media: Verif_VP_28.pdf|Блок 28.]] Символьный алгоритм model checking для CTL (окончание).
 +
 
 +
[[Media: Verif_VP_29.pdf|Блок 29.]] CTL*. CTL и LTL как фрагменты CTL*. Сравнение выразительности CTL и LTL.
 +
 
 +
[[Media: Verif_VP_30.pdf|Блок 30.]] Системы реального времени (СРВ). Временные автоматы.
 +
 
 +
[[Media: Verif_VP_31.pdf|Блок 31.]] Неправдоподобные вычисления временных автоматов.
 +
 
 +
[[Media: Verif_VP_32.pdf|Блок 32.]] Логика ветвящегося реального времени (TCTL). Задача model checking для TCTL.
 +
 
 +
[[Media: Verif_VP_33.pdf|Блок 33.]] Сети временных автоматов.
 +
 
 +
[[Media: Verif_VP_34.pdf|Блок 34.]] Алгоритм model checking для TCTL. Временные регионы. Системы регионов.
 +
 
 +
[[Media: Verif_VP_35.pdf|Блок 35.]] Отношения симуляции и бисимуляции. Симуляционная и бисимуляционная эквивалентности.
 +
 
 +
[[Media: Verif_VP_36.pdf|Блок 36.]] Бисимуляция состояний модели. Алгоритм проверки бисимуляционной эквивалентности. Фактор-модель.
 +
 
 +
''Материалы будут появляться по мере проведения занятий.''
 +
 
 +
== Прошлогодние ==
 +
 
 +
[[Media: Verif_VP_37.pdf|Блок 37.]] Абстракция моделей. Редукция по конусу влияния. Абстракция данных.
 +
 
 +
[[Media: Verif_VP_38.pdf|Блок 38.]] Bounded model checking (BMC), постановка.
 +
 
 +
[[Media: Verif_VP_39.pdf|Блок 39.]] Проблема выполнимости булевых формул (SAT).
 +
 
 +
[[Media: Verif_VP_40.pdf|Блок 40.]] Решение BMC с помощью SAT.
 +
 
 +
[[Media: Verif_VP_all.pdf|Все слайды лекций в одном файле.]]
 +
 
 +
= Семинары =
 +
 
 +
[[Media: Verif_VP_sem01.pdf|Семинар 1.]] Дедуктивная верификация императивных программ.
 +
 
 +
[[Media: Verif_VP_sem02.pdf|Семинар 2.]] Модели Крипке. LTL. Безопасность и живость. Справедливость.
 +
 
 +
[[Media: Verif_VP_sem03.pdf|Семинар 3.]] CTL. Базовый алгоритм model checking для CTL. BDD.
 +
 
 +
''Материалы будут появляться по мере проведения занятий.''
 +
 
 +
= Обязательные домашние задания =
 +
 
 +
Курсом предполагаются три обязательных домашних задания: "Spin", "NuSMV", "Uppaal".
 +
Невыполнение этих заданий влечёт за собой снижение итоговой экзаменационной оценки:
 +
* Если выполнены ровно два задания, то итоговая оценка снижается на 1:
 +
** "отлично" -> "хорошо";
 +
** "хорошо" -> "удовлетворительно";
 +
** "удовлетворительно" -> "неудовлетворительно".
 +
* Если выполнено менее двух заданий, то итоговая оценка снижается на 2:
 +
** "отлично" -> "удовлетворительно";
 +
** "хорошо" -> "неудовлетворительно";
 +
** "удовлетворительно" -> "неудовлетворительно".
 +
 
 +
== Материалы занятий ==
 +
 
 +
[[Media: Verif_VP_Review_Spin.pdf|Блок О1.]] Обзор средства Spin.
 +
 
 +
[[Media: Verif_VP_Prac_Spin.pdf|Семинар О1.]] Упражнения для Spin.
 +
 
 +
[[Media: Verif_VP_Review_Nusmv.pdf|Блок О2.]] Обзор средства NuSMV.
 +
 
 +
[[Media: Verif_VP_Prac_Nusmv.pdf|Семинар О2.]] Средство NuSMV.
 +
 
 +
[[Media: Verif_VP_Prac_Uppaal.pdf|Семинар О3.]] Средство Uppaal.
 +
 
 +
[[Media: Verif_VP_Prac_Uppaal.zip|Дополнительные материалы к семинару О3.]]
 +
 
 +
''Материалы будут появляться по мере проведения занятий.''
 +
 
 +
== Установка средств верификации ==
 +
 
 +
Для выполнения обязательных домашних заданий необходимо поставить на свою рабочую машину средства
 +
* [http://spinroot.com Spin],
 +
* [http://nusmv.fbk.eu NuSMV],
 +
* [http://uppaal.org UPPAAL] (''лучше версию 4.1 ("development snapshot")'').
 +
 
 +
Рекомендуется всё это поставить в Linux - иначе могут возникать странные технические проблемы и препятствия.
 +
 
 +
После установки средств желательно проверить, что они работают:
 +
* "'''./spin -a <папка с примерами spin>/LTL/bakery.pml'''" успешно завершает работу без вывода;
 +
* в выводе "'''./NuSMV'''" есть строки, утверждающие, что
 +
** подключены CUDD и MiniSat, либо нет строк о том, что что-то надо подключить, и
 +
** входной файл не подан и работа завершена;
 +
* "'''./uppaal'''" загружает графический интерфейс и для какого-нибудь примера при нажатии на кнопку '''Check''' вкладки '''Verifier''' при каком-нибудь выделенном свойстве завершает вывод словами '''Property is satisfied''' или '''Property is not satisfied'''.
 +
 
 +
Для полноценной работы на семинарах, посвящённых средствам верификации, требуется принести и использовать свой ноутбук (или хотя бы ноутбук соседа).
 +
Участие без ноутбука тоже возможно: слушать и смотреть, но без возможности воспроизвести обсуждаемое или попробовать что-то своё.
 +
 
 +
== Общие правила выполнения заданий "NuSMV", "Spin", "Uppaal" ==
 +
 
 +
Задания можно выполнять в одиночку или вдвоём.
 +
Для получения задания следует отправить [[Подымов Владислав Васильевич|ему]] на почту письмо с любым текстом и заголовком в следующем формате ('''ZZ''' заменяется на '''spin''', '''nusmv''' или '''uppaal''' в зависимости от того, какое задание запрашивается):
 +
* '''[ver-ZZ] группа Фамилия И.О.''' для выполнения в одиночку.
 +
* '''[ver-ZZ] группа Фамилия И.О., Фамилия И.О.''' для выполнения вдвоём.
 +
В ответ будет выслано письмо с системой и целями её исследования при помощи проверки требований.
 +
 
 +
В тексте письма можно выразить пожелания о том, какого рода задание хочется, вплоть до точной формулировки.
 +
Разумные пожелания будут учтены по возможности.
 +
Типовые примеры пожеланий: примеры пожеланий: "хочу исследовать параллельно работающие программы", "... схему", "... игру/головоломку", "... систему общего вида, без программистско-математической специализации".
 +
 
 +
Срок выполнения заданий:
 +
* Вплоть до экзамена, пока лектору не надоест их принимать.
 +
* Если всё сдано до конца семестра, то выдаётся небольшое поощрение (технические баллы к экзамену).
 +
* Если каждое задание сдано до соответствующего крайнего срока в плане занятий, то выдаётся чуть большее поощрение.
 +
 
 +
Присланное решение принимается, не принимается или отправляется на доработку в зависимости от того, насколько оно правильно и, если есть ошибки, насколько хорошо в нём видны осознанные попытки разобраться в принципах работы со средством верификации.
 +
 
 +
== NuSMV ==
 +
 
 +
Решение этого задания - это
 +
* файл с расширением ".smv", содержащий формализацию системы и требований в формате средства NuSMV, и
 +
* пояснение того, как результаты проверки требований, выдаваемые NuSMV, соотносятся с поставленными целями, в свободной форме.
 +
 
 +
== Spin ==
 +
 
 +
Решение этого задания - это
 +
* файл с расширением ".pml", содержащий формализацию системы и требований на языке PROMELA, и
 +
* пояснение того, как результаты проверки требований, выдаваемые средством Spin, соотносятся с поставленными целями, в свободной форме.
 +
 
 +
== Uppaal ==
 +
 
 +
Решение этого задания - это
 +
* файл или файлы, сгенерированные средством Uppaal и содержащие формализацию системы и требований (Uppaal 4.1: файл ".xml"; Uppaal 4.0: файлы ".xml" и ".q"), и
 +
* пояснение того, как результаты проверки требований, выдаваемые средством Uppaal, соотносятся с поставленными целями, в свободной форме.
 +
 
 +
= Правила проведения экзамена =
 +
 
 +
Итоговая экзаменационная оценка складывается из
 +
* оценки за экзаменационную контрольную работу,
 +
* зачетных оценок за выполнение [[#Обязательные домашние задания|обязательных домашних заданий]] и
 +
* оценок за решение [[#Премиальные задачи|премиальных задач]].
 +
 
 +
Экзаменационная контрольная работа проводится письменно, длительность - 150 минут, и состоит из 5 практических и 5 теоретических задач.
 +
Каждая из практических задач относится к одному из типов, которые разбирались на семинарах или в лекциях.
 +
Каждая из теоретических задач касается формулировок определений или ключевых результатов, рассмотренных в лекциях.
 +
 
 +
= Премиальные задачи =
 +
 
 +
Крайний срок выполнения всех премиальных задач - конец семестра.
 +
 
 +
== Лекционные премиальные задачи ==
 +
 
 +
Эти задачи явно обозначаются в слайдах лекций.
 +
 
 +
== Логика Хоара ==
 +
 
 +
Задание сформулировано на последнем слайде материалов семинара 1.
 +
 
 +
Выполнившие это задание освобождаются от решения задачи на тему логики Хоара на экзамене и могут быть поощрены дополнительно за особые заслуги.
 +
 
 +
== CTL: формализация требований и алгоритмы проверки формул ==
 +
 
 +
Если написать письмо с любым содержанием и заголовком '''[ver-ctl] группа Фамилия И.О.''', то в ответ будут присланы описание системы и требований к этой системе.
 +
Требуется адекватно формализовать требования в логике ветвящегося времени и изобразить шаги работы базового или символьного алгоритма.
 +
 
 +
Если сомневаетесь, что означает "изобразить шаги работы алгоритма", то по умолчанию поступайте так:
 +
* базовый алгоритм:
 +
** нарисовать модель Крипке, адекватно описывающую систему;
 +
** описать пошаговое получение информации о выполнимости подформул алгоритмом настолько (''не'')строго, чтобы можно было без чрезмерных усилий строго восстановить каждый шаг работы алгоритма;
 +
* символьный алгоритм:
 +
** описать символьное представление модели Крипке (основанной на любом общеизвестном представлении булевых функций);
 +
** описать пошаговое преобразование символьных записей алгоритмом настолько (''не'')строго, чтобы можно было без чрезмерных усилий строго восстановить каждый шаг работы алгоритма.
 +
 
 +
Выполнившие это задание освобождаются от задач, темы которых покрываются этим заданием, и могут быть поощрены дополнительно за особые заслуги (например, за хорошее понимание устройства символьного алгоритма).
 +
 
 +
== CTL и справедливость ==
 +
 
 +
Это '''трудное''' домашнее задание.
 +
 
 +
При выполнении этого задания автоматически засчитывается часть задания "CTL: формализация требований и алгоритмы проверки формул", относящаяся к изображению шагов работы алгоритма.
 +
 
 +
Требуется:
 +
* предложить описание символьного алгоритма верификации CTL-формул, работающего в условиях справедливости для CTL:
 +
** можно написать псевдокод с пояснениями,
 +
** можно описать на естественном языке, но так, чтобы можно было без чрезмерных усилий строго восстановить каждый шаг работы алгоритма,
 +
** можно написать программу,
 +
** ...;
 +
* привести пример работы алгоритма, иллюстрирующий его отличие от "несправедливого" символьного алгоритма.
 +
 
 +
= Литература =
 +
 
 +
#Э.М. Кларк, О. Грамберг, Д. Пелед. Верификация моделей программ: Model Checking. Изд-во МЦНМО, 2002.
 +
#Ю.Г. Карпов. Model Checking: верификация параллельных и распределенных программных систем. Изд-во БХВ-Петербург, 2010.
 +
#K. R. Apt, E.-R. Olderog. Verification of sequential and concurrent programs, Springer, 1997.
 +
#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.
 +
#Baier C., Katoen J.-P. Principles of model checking, MIT Press, 2008.
 +
#Clarke E., Henzinger T.A., Veith H., Bloem R. Handbook of model checking, Springer, 2018.

Текущая версия на 13:26, 17 ноября 2024

Актуальность информации: осенний семестр 2024/2025 учебного года.

Обязательный курс для магистров групп 618мк_дса, 618мк_дус и 621асвк 3 семестра магистратуры (группа 621асвк - "Методы верификации программ"). Курс читает В. В. Подымов.

Лекции

Блок 1 (вводный). Что такое и зачем нужна формальная верификация.

Блок 2. Логика предикатов (напоминание).

Блок 3. Общие принципы дедуктивной верификации программ. Модельные императивные программы: синтаксис, операционная семантика.

Блок 4. Дедуктивная верификация программ: постановка задачи, логика Хоара.

Блок 5. Дедуктивная верификация программ: аннотированные программы.

Блок 6. Дедуктивная верификация программ: возможности автоматизации, слабейшее предусловие.

Блок 7. Общая схема метода model checking.

Блок 8. Модели Крипке.

Блок 9. Особенности моделирования систем.

Блок 10. Пара слов о последовательностях.

Блок 11. Свойства трасс. Безопасность и живость.

Блок 12. Логика линейного времени (LTL). Постановка задачи верификации моделей Крипке относительно LTL.

Блок 13. Размеченные системы переходов. Справедливость для систем переходов. Справедливость в LTL.

Блок 14. Автоматный алгоритм model checking для LTL: общая схема.

Блок 15. Автоматы Бюхи. Обобщённые автоматы Бюхи.

Блок 16. Пересечение автоматов Бюхи.

Блок 17. Проверка пустоты автомата Бюхи.

Блок 18. Автоматы Бюхи для моделей Крипке

Блок 19. Автоматы Бюхи для ltl-формул.

Блок 20. Автоматный алгоритм model checking для LTL: уточнённая схема.

Блок 21. Логика деревьев вычислений (CTL). Постановка задачи верификации моделей Крипке относительно CTL.

Блок 22. Базовый алгоритм model checking для CTL.

Блок 23. Справедливость и CTL.

Блок 24. Символьные представления моделей.

Блок 25. Двоичные решающие диаграммы: BDD, OBDD, ROBDD.

Блок 26. Символьный алгоритм model checking для CTL (начало).

Блок 27. Преобразователи предикатов и их неподвижные точки.

Блок 28. Символьный алгоритм model checking для CTL (окончание).

Блок 29. CTL*. CTL и LTL как фрагменты CTL*. Сравнение выразительности CTL и LTL.

Блок 30. Системы реального времени (СРВ). Временные автоматы.

Блок 31. Неправдоподобные вычисления временных автоматов.

Блок 32. Логика ветвящегося реального времени (TCTL). Задача model checking для TCTL.

Блок 33. Сети временных автоматов.

Блок 34. Алгоритм model checking для TCTL. Временные регионы. Системы регионов.

Блок 35. Отношения симуляции и бисимуляции. Симуляционная и бисимуляционная эквивалентности.

Блок 36. Бисимуляция состояний модели. Алгоритм проверки бисимуляционной эквивалентности. Фактор-модель.

Материалы будут появляться по мере проведения занятий.

Прошлогодние

Блок 37. Абстракция моделей. Редукция по конусу влияния. Абстракция данных.

Блок 38. Bounded model checking (BMC), постановка.

Блок 39. Проблема выполнимости булевых формул (SAT).

Блок 40. Решение BMC с помощью SAT.

Все слайды лекций в одном файле.

Семинары

Семинар 1. Дедуктивная верификация императивных программ.

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

Семинар 3. CTL. Базовый алгоритм model checking для CTL. BDD.

Материалы будут появляться по мере проведения занятий.

Обязательные домашние задания

Курсом предполагаются три обязательных домашних задания: "Spin", "NuSMV", "Uppaal". Невыполнение этих заданий влечёт за собой снижение итоговой экзаменационной оценки:

  • Если выполнены ровно два задания, то итоговая оценка снижается на 1:
    • "отлично" -> "хорошо";
    • "хорошо" -> "удовлетворительно";
    • "удовлетворительно" -> "неудовлетворительно".
  • Если выполнено менее двух заданий, то итоговая оценка снижается на 2:
    • "отлично" -> "удовлетворительно";
    • "хорошо" -> "неудовлетворительно";
    • "удовлетворительно" -> "неудовлетворительно".

Материалы занятий

Блок О1. Обзор средства Spin.

Семинар О1. Упражнения для Spin.

Блок О2. Обзор средства NuSMV.

Семинар О2. Средство NuSMV.

Семинар О3. Средство Uppaal.

Дополнительные материалы к семинару О3.

Материалы будут появляться по мере проведения занятий.

Установка средств верификации

Для выполнения обязательных домашних заданий необходимо поставить на свою рабочую машину средства

  • Spin,
  • NuSMV,
  • UPPAAL (лучше версию 4.1 ("development snapshot")).

Рекомендуется всё это поставить в Linux - иначе могут возникать странные технические проблемы и препятствия.

После установки средств желательно проверить, что они работают:

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

Для полноценной работы на семинарах, посвящённых средствам верификации, требуется принести и использовать свой ноутбук (или хотя бы ноутбук соседа). Участие без ноутбука тоже возможно: слушать и смотреть, но без возможности воспроизвести обсуждаемое или попробовать что-то своё.

Общие правила выполнения заданий "NuSMV", "Spin", "Uppaal"

Задания можно выполнять в одиночку или вдвоём. Для получения задания следует отправить ему на почту письмо с любым текстом и заголовком в следующем формате (ZZ заменяется на spin, nusmv или uppaal в зависимости от того, какое задание запрашивается):

  • [ver-ZZ] группа Фамилия И.О. для выполнения в одиночку.
  • [ver-ZZ] группа Фамилия И.О., Фамилия И.О. для выполнения вдвоём.

В ответ будет выслано письмо с системой и целями её исследования при помощи проверки требований.

В тексте письма можно выразить пожелания о том, какого рода задание хочется, вплоть до точной формулировки. Разумные пожелания будут учтены по возможности. Типовые примеры пожеланий: примеры пожеланий: "хочу исследовать параллельно работающие программы", "... схему", "... игру/головоломку", "... систему общего вида, без программистско-математической специализации".

Срок выполнения заданий:

  • Вплоть до экзамена, пока лектору не надоест их принимать.
  • Если всё сдано до конца семестра, то выдаётся небольшое поощрение (технические баллы к экзамену).
  • Если каждое задание сдано до соответствующего крайнего срока в плане занятий, то выдаётся чуть большее поощрение.

Присланное решение принимается, не принимается или отправляется на доработку в зависимости от того, насколько оно правильно и, если есть ошибки, насколько хорошо в нём видны осознанные попытки разобраться в принципах работы со средством верификации.

NuSMV

Решение этого задания - это

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

Spin

Решение этого задания - это

  • файл с расширением ".pml", содержащий формализацию системы и требований на языке PROMELA, и
  • пояснение того, как результаты проверки требований, выдаваемые средством Spin, соотносятся с поставленными целями, в свободной форме.

Uppaal

Решение этого задания - это

  • файл или файлы, сгенерированные средством Uppaal и содержащие формализацию системы и требований (Uppaal 4.1: файл ".xml"; Uppaal 4.0: файлы ".xml" и ".q"), и
  • пояснение того, как результаты проверки требований, выдаваемые средством Uppaal, соотносятся с поставленными целями, в свободной форме.

Правила проведения экзамена

Итоговая экзаменационная оценка складывается из

Экзаменационная контрольная работа проводится письменно, длительность - 150 минут, и состоит из 5 практических и 5 теоретических задач. Каждая из практических задач относится к одному из типов, которые разбирались на семинарах или в лекциях. Каждая из теоретических задач касается формулировок определений или ключевых результатов, рассмотренных в лекциях.

Премиальные задачи

Крайний срок выполнения всех премиальных задач - конец семестра.

Лекционные премиальные задачи

Эти задачи явно обозначаются в слайдах лекций.

Логика Хоара

Задание сформулировано на последнем слайде материалов семинара 1.

Выполнившие это задание освобождаются от решения задачи на тему логики Хоара на экзамене и могут быть поощрены дополнительно за особые заслуги.

CTL: формализация требований и алгоритмы проверки формул

Если написать письмо с любым содержанием и заголовком [ver-ctl] группа Фамилия И.О., то в ответ будут присланы описание системы и требований к этой системе. Требуется адекватно формализовать требования в логике ветвящегося времени и изобразить шаги работы базового или символьного алгоритма.

Если сомневаетесь, что означает "изобразить шаги работы алгоритма", то по умолчанию поступайте так:

  • базовый алгоритм:
    • нарисовать модель Крипке, адекватно описывающую систему;
    • описать пошаговое получение информации о выполнимости подформул алгоритмом настолько (не)строго, чтобы можно было без чрезмерных усилий строго восстановить каждый шаг работы алгоритма;
  • символьный алгоритм:
    • описать символьное представление модели Крипке (основанной на любом общеизвестном представлении булевых функций);
    • описать пошаговое преобразование символьных записей алгоритмом настолько (не)строго, чтобы можно было без чрезмерных усилий строго восстановить каждый шаг работы алгоритма.

Выполнившие это задание освобождаются от задач, темы которых покрываются этим заданием, и могут быть поощрены дополнительно за особые заслуги (например, за хорошее понимание устройства символьного алгоритма).

CTL и справедливость

Это трудное домашнее задание.

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

Требуется:

  • предложить описание символьного алгоритма верификации CTL-формул, работающего в условиях справедливости для 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.
  6. Clarke E., Henzinger T.A., Veith H., Bloem R. Handbook of model checking, Springer, 2018.
Источник — «https://mk.cs.msu.ru/index.php?title=Математические_методы_верификации_схем_и_программ&oldid=11549»