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

Материал из Кафедра математической кибернетики
Перейти к: навигация, поиск
 
(не показаны 64 промежуточных версий 1 участника)
Строка 1: Строка 1:
 +
[[Категория:Спецкурсы кафедры МК]]
 
[[Категория:Лекционные курсы кафедры МК]]
 
[[Категория:Лекционные курсы кафедры МК]]
 
[[Категория:Магистерская программа Дискретные управляющие системы и их приложения]]
 
[[Категория:Магистерская программа Дискретные управляющие системы и их приложения]]
−
''Актуальность информации: осенний семестр 2022/2023 учебного года.''
+
''Актуальность информации: осенний семестр 2025/2026 учебного года.''
  
−
Обязательный курс для магистров групп 618мк_дс, 618мк_дус и 621асвк 3 семестра магистратуры (группа 621асвк - "Методы верификации программ").  
+
Обязательный курс для магистров групп 618мк_дса, 618мк_дус и 621асвк 3 семестра магистратуры (группа 621асвк - "Методы верификации программ").  
 
Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].
 
Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].
  
−
= Лекции =
+
= Материалы занятий =
  
−
[[Media: Verif_VP_01.pdf|Блок 1]] (вводная). Что такое и зачем нужна формальная верификация.
+
== Лекции ==
  
−
[[Media: Verif_VP_02.pdf|Блок 2.]] Общие принципы дедуктивной верификации программ. Модельные императивные программы: синтаксис, операционная семантика.
+
[[Media: Verif_VP_01.pdf|Блок 1]] (вводный). Что такое и зачем нужна формальная верификация.
  
−
[[Media: Verif_VP_03.pdf|Блок 3.]] Дедуктивная верификация программ: постановка задачи, логика Хоара.
+
[[Media: Verif_VP_02.pdf|Блок 2.]] Логика предикатов (напоминание).
  
−
[[Media: Verif_VP_04.pdf|Блок 4.]] Дедуктивная верификация программ: аннотированные программы.
+
[[Media: Verif_VP_03.pdf|Блок 3.]] Общие принципы дедуктивной верификации программ. Модельные императивные программы: синтаксис, операционная семантика.
  
−
[[Media: Verif_VP_05.pdf|Блок 5.]] Дедуктивная верификация программ: возможности автоматизации, слабейшее предусловие.
+
[[Media: Verif_VP_04.pdf|Блок 4.]] Дедуктивная верификация программ: постановка задачи, логика Хоара.
  
−
[[Media: Verif_VP_06.pdf|Блок 6.]] Общая схема метода model checking.
+
[[Media: Verif_VP_05.pdf|Блок 5.]] Дедуктивная верификация программ: аннотированные программы.
  
−
[[Media: Verif_VP_07.pdf|Блок 7.]] Модели Крипке. Особенности моделирования систем.
+
[[Media: Verif_VP_06.pdf|Блок 6.]] Дедуктивная верификация программ: возможности автоматизации, слабейшее предусловие.
  
−
[[Media: Verif_VP_08.pdf|Блок 8.]] Свойства трасс. Безопасность и живость.
+
[[Media: Verif_VP_07.pdf|Блок 7.]] Общая схема метода model checking.
  
−
[[Media: Verif_VP_09.pdf|Блок 9.]] Логика линейного времени (LTL). Постановка задачи верификации моделей Крипке относительно LTL.
+
[[Media: Verif_VP_08.pdf|Блок 8.]] Модели Крипке.
  
−
[[Media: Verif_VP_10.pdf|Блок 10.]] Размеченные системы переходов. Справедливость для систем переходов. Справедливость и LTL.
+
[[Media: Verif_VP_09.pdf|Блок 9.]] Особенности моделирования систем.
  
−
[[Media: Verif_VP_11.pdf|Блок 11.]] Автоматный алгоритм model checking для LTL: общая схема.
+
[[Media: Verif_VP_10.pdf|Блок 10.]] Пара слов о последовательностях.
  
−
[[Media: Verif_VP_12.pdf|Блок 12.]] Автоматы Бюхи. Обобщённые автоматы Бюхи.
+
[[Media: Verif_VP_11.pdf|Блок 11.]] Свойства трасс. Безопасность и живость.
  
−
[[Media: Verif_VP_13.pdf|Блок 13.]] Пересечение автоматов Бюхи. Проверка пустоты автомата Бюхи.
+
[[Media: Verif_VP_12.pdf|Блок 12.]] Логика линейного времени (LTL). Постановка задачи верификации моделей Крипке относительно LTL.
  
−
[[Media: Verif_VP_14.pdf|Блок 14.]] Автоматы Бюхи для моделей Крипке и ltl-формул.
+
[[Media: Verif_VP_13.pdf|Блок 13.]] Размеченные системы переходов. Справедливость для систем переходов. Справедливость в LTL.
  
−
[[Media: Verif_VP_15.pdf|Блок 15.]] Автоматный алгоритм model checking для LTL: уточнённая схема.
+
[[Media: Verif_VP_14.pdf|Блок 14.]] Автоматный алгоритм model checking для LTL: общая схема.
  
−
[[Media: Verif_VP_Review_Spin.pdf|Блок О1.]] Обзор средства Spin.
+
[[Media: Verif_VP_15.pdf|Блок 15.]] Автоматы Бюхи. Обобщённые автоматы Бюхи.
  
−
[[Media: Verif_VP_16.pdf|Блок 16.]] Логика деревьев вычислений (CTL). Постановка задачи верификации моделей Крипке относительно CTL.
+
[[Media: Verif_VP_16.pdf|Блок 16.]] Пересечение автоматов Бюхи.
  
−
[[Media: Verif_VP_17.pdf|Блок 17.]] Базовый алгоритм model checking для CTL.
+
[[Media: Verif_VP_17.pdf|Блок 17.]] Проверка пустоты автомата Бюхи.
  
−
[[Media: Verif_VP_18.pdf|Блок 18.]] Справедливость и CTL.
+
[[Media: Verif_VP_18.pdf|Блок 18.]] Автоматы Бюхи для моделей Крипке
  
−
[[Media: Verif_VP_19.pdf|Блок 19.]] Символьные представления моделей.
+
[[Media: Verif_VP_19.pdf|Блок 19.]] Автоматы Бюхи для ltl-формул.
  
−
[[Media: Verif_VP_20.pdf|Блок 20.]] Двоичные решающие диаграммы: BDD, OBDD, ROBDD.
+
[[Media: Verif_VP_20.pdf|Блок 20.]] Автоматный алгоритм model checking для LTL: уточнённая схема.
  
−
[[Media: Verif_VP_21.pdf|Блок 21.]] Символьный алгоритм model checking для CTL. Преобразователи предикатов. Неподвижные точки.
+
[[Media: Verif_VP_21.pdf|Блок 21.]] Логика деревьев вычислений (CTL). Постановка задачи верификации моделей Крипке относительно CTL.
  
−
[[Media: Verif_VP_Review_Nusmv.pdf|Блок О2.]] Обзор средства NuSMV.
+
[[Media: Verif_VP_22.pdf|Блок 22.]] Базовый алгоритм model checking для CTL.
  
−
[[Media: Verif_VP_22.pdf|Блок 22.]] CTL*. CTL и LTL как фрагменты CTL*. Сравнение выразительности CTL и LTL.
+
[[Media: Verif_VP_23.pdf|Блок 23.]] Справедливость и CTL.
  
−
[[Media: Verif_VP_23.pdf|Блок 23.]] Системы реального времени. Временные автоматы. Неправдоподобные вычисления временных автоматов.
+
[[Media: Verif_VP_24.pdf|Блок 24.]] Символьные представления моделей.
  
−
[[Media: Verif_VP_24.pdf|Блок 24.]] Логика ветвящегося реального времени (TCTL). Задача model checking для TCTL.
+
[[Media: Verif_VP_25.pdf|Блок 25.]] Символьный алгоритм model checking для CTL (начало).
  
−
[[Media: Verif_VP_25.pdf|Блок 25.]] Алгоритм model checking для TCTL. Временные регионы. Системы регионов.
+
[[Media: Verif_VP_26.pdf|Блок 26.]] Преобразователи предикатов и их неподвижные точки.
  
−
[[Media: Verif_VP_26.pdf|Блок 26.]] Сети временных автоматов.
+
[[Media: Verif_VP_27.pdf|Блок 27.]] Символьный алгоритм model checking для CTL (окончание).
  
−
''Слайды лекций будут появляться по мере проведения занятий.''
+
[[Media: Verif_VP_28.pdf|Блок 28.]] CTL*. CTL и LTL как фрагменты CTL*. Сравнение выразительности CTL и LTL.
  
−
= Семинары =
+
[[Media: Verif_VP_29.pdf|Блок 29.]] Системы реального времени (СРВ). Временные автоматы.
 +
 
 +
[[Media: Verif_VP_30.pdf|Блок 30.]] Неправдоподобные вычисления временных автоматов.
 +
 
 +
[[Media: Verif_VP_31.pdf|Блок 31.]] Логика ветвящегося реального времени (TCTL). Задача model checking для TCTL.
 +
 
 +
[[Media: Verif_VP_32.pdf|Блок 32.]] Сети временных автоматов.
 +
 
 +
[[Media: Verif_VP_33.pdf|Блок 33.]] Алгоритм model checking для TCTL. Временные регионы. Системы регионов.
 +
 
 +
[[Media: Verif_VP_34.pdf|Блок 34.]] Отношения симуляции и бисимуляции. Симуляционная и бисимуляционная эквивалентности.
 +
 
 +
''Материалы будут появляться по мере проведения занятий.''
 +
 
 +
=== Прошлогодние ===
 +
 
 +
[[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_sem01.pdf|Семинар 1.]] Дедуктивная верификация императивных программ.
Строка 72: Строка 101:
 
[[Media: Verif_VP_sem02.pdf|Семинар 2.]] Модели Крипке. LTL. Безопасность и живость. Справедливость.
 
[[Media: Verif_VP_sem02.pdf|Семинар 2.]] Модели Крипке. LTL. Безопасность и живость. Справедливость.
  
−
[[Media: Verif_VP_Prac_Spin.pdf|Семинар О1.]] Средство Spin.
+
[[Media: Verif_VP_sem03.pdf|Семинар 3.]] CTL. Базовый алгоритм model checking для CTL.
  
−
[[Media: Seminar_Verification_7_spin_manual.pdf| (Устаревшее) Несколько инструкций относительно Spin.]]
+
== Обязательные домашние задания ==
  
−
[[Media: Verif_VP_sem03.pdf|Семинар 3.]] CTL. Базовый алгоритм model checking для CTL. BDD.
+
[[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_Nusmv.pdf|Семинар О2.]] Средство NuSMV.
  
−
''Материалы будут обновляться по мере проведения занятий.''
+
[[Media: Verif_VP_Prac_Uppaal.pdf|Семинар О3.]] Средство Uppaal.
  
−
'''[[Media: Seminar_Verification_10_eng.pdf| Seminar 10-11.]]''' UPPAAL exercises.
+
[[Media: Verif_VP_Prac_Uppaal.zip|Дополнительные материалы к семинару О3.]]
  
−
'''[[Media: Seminar_Verification_10_errors.zip| Zip-file required for the last exercises of Seminar 10-11.]]
+
''Материалы будут появляться по мере проведения занятий.''
  
−
= Правила проведения экзамена =
+
= Экзамен =
 +
 
 +
Экзамен проводится письменно, длительность - 120 минут.
 +
Экзаменационная работа состоит из следующих задач:
 +
* 3 задачи, разбиравшиеся на семинарах: доказать частичную корректность программы, формализовать предложение в LTL, проверить выполнимость формулы CTL на модели.
 +
* 6 задач, относящихся к лекциям. В этих задачах могут проверяться, в числе прочего, знания определений и формулировок, умение применять алгоритмы (даже если соответствующих задач не было на семинарах) и углублённое понимание материалов (вопросы на понимание).
  
 
Итоговая экзаменационная оценка складывается из
 
Итоговая экзаменационная оценка складывается из
−
* оценки за экзаменационную контрольную работу,
+
* оценки за экзаменационную работу,
−
* зачетных оценок за выполнение [[#Обязательные домашние задания|обязательных домашних заданий]] и
+
* оценок за решение [[#Премиальные задачи|премиальных задач]] и
−
* оценок за решение [[#Премиальные задачи|премиальных задач]].
+
* зачетных оценок за выполнение [[#Обязательные домашние задания|обязательных домашних заданий]].
 +
 
 +
Каждая экзаменационная задача оценивается по шкале от 0 до 4 баллов.
 +
Эти баллы суммируются, и к ним прибавляются баллы за премиальные задачи.
 +
Оценка за экзамен зависит от суммарного балла и от сдачи обязательных заданий так:
  
−
Экзаменационная контрольная работа состоит из 5 практических задач и 5 вопросов.
+
{|class="wikitable"
−
Каждая из практических задач относится к одному из типов, которые разбирались на семинарах или в лекциях.
+
|
−
Каждый из вопросов касается формулировок определений или ключевых результатов, рассмотренных в лекциях.
+
|
 +
!colspan="3"|Количество зачтённых обязательных заданий
 +
|-
 +
|
 +
|
 +
| 3
 +
| 2
 +
| 1 или 0
 +
|-
 +
!rowspan="4"|Баллы
 +
| 29 или больше
 +
| Отлично
 +
| Хорошо
 +
| Удовлетворительно
 +
|-
 +
| 22-28
 +
| Хорошо
 +
| Удовлетворительно
 +
| Неудовлетворительно
 +
|-
 +
| 15-21
 +
| Удовлетворительно
 +
| Неудовлетворительно
 +
| Неудовлетворительно
 +
|-
 +
| меньше 15
 +
| Неудовлетворительно
 +
| Неудовлетворительно
 +
| Неудовлетворительно
 +
|}
  
 
= Обязательные домашние задания =
 
= Обязательные домашние задания =
  
−
Курсом предполагаются три обязательных домашних задания: "NuSMV", "Spin" и "Uppaal".
+
Курсом предполагаются три обязательных домашних задания: "Spin", "NuSMV", "Uppaal".
−
Невыполнение этих заданий влечёт за собой снижение итоговой экзаменационной оценки:
+
−
* Если выполнены ровно два задания, то итоговая оценка снижается на 1:
+
−
** "отлично" -> "хорошо";
+
−
** "хорошо" -> "удовлетворительно";
+
−
** "удовлетворительно" -> "неудовлетворительно".
+
−
* Если выполнено менее двух заданий, то итоговая оценка снижается на 2:
+
−
** "отлично" -> "удовлетворительно";
+
−
** "хорошо" -> "неудовлетворительно";
+
−
** "удовлетворительно" -> "неудовлетворительно".
+
  
 
== Установка средств верификации ==
 
== Установка средств верификации ==
  
−
* Для выполнения обязательных домашних заданий необходимо поставить на свою рабочую машину средства [http://nusmv.fbk.eu NuSMV], [http://spinroot.com Spin] и [http://uppaal.org UPPAAL] (''лучше версию 4.1 ("development snapshot")'').
+
Для выполнения обязательных домашних заданий необходимо поставить на свою рабочую машину средства
−
* Рекомендуется всё это поставить в Linux (''с Windows у студентов регулярно возникают странные проблемы, а в Linux всё работает - проверено'').
+
* [http://spinroot.com Spin],
−
* После установки средств желательно проверить, что они работают:
+
* [http://nusmv.fbk.eu NuSMV],
−
** в выводе "'''./NuSMV'''" есть строки, утверждающие, что
+
* [http://uppaal.org UPPAAL].
−
*** подключены CUDD и MiniSat, либо нет строк о том, что что-то надо подключить, и
+
−
*** входной файл не подан и работа завершена;
+
−
** "'''./spin -a <папка с примерами spin>/LTL/bakery.pml'''" успешно завершает работу без вывода;
+
−
** "'''./uppaal'''" загружает графический интерфейс и для какого-нибудь примера при нажатии на кнопку '''Check''' вкладки '''Verifier''' при каком-нибудь выделенном свойстве завершает вывод словами '''Property is satisfied''' или '''Property is not satisfied'''.
+
−
* '''Для работы на семинарах, посвящённых средствам верификации, требуется организовать хотя бы один ноутбук на двоих (если совсем не выходит, то на троих) с установленными соответствующими средствами верификации.'''
+
  
−
== Общие правила выполнения заданий "NuSMV", "Spin" и "Uppaal" ==
+
Рекомендуется всё это поставить в Linux - иначе могут возникать странные технические проблемы и излишние препятствия.
  
−
* Каждое из заданий можно выполнять как в одиночку, так и в паре.
+
После установки средств желательно проверить, что они работают:
−
* Срок выполнения задания (кроме индивидуально согласованных случаев) - от начала проведения соответствующих семинаров и до начала проведения следующего тематического блока семинаров (для последнего блока семинаров - до окончания семестра).
+
* "'''./spin -a <папка с примерами spin>/LTL/bakery.pml'''" успешно завершает работу без вывода;
−
* Первый шаг выполнения - выслать [[Подымов Владислав Васильевич|ему]] на почту письмо с любым текстом и специальным заголовком:
+
* в выводе "'''./NuSMV'''" есть строки, утверждающие, что
−
** для выполнения задания "NuSMV" в одиночку: '''[ver-nusmv] группа Фамилия И.О.'''
+
** подключены CUDD и MiniSat, либо нет строк о том, что что-то надо подключить, и
−
** для выполнения задания "NuSMV" в паре: '''[ver-nusmv] группа Фамилия И.О., Фамилия И.О.'''
+
** входной файл не подан и работа завершена;
−
** для выполнения задания "Spin" в одиночку: '''[ver-spin] группа Фамилия И.О.'''
+
* "'''./uppaal'''" загружает графический интерфейс и для какого-нибудь примера при нажатии на кнопку '''Check''' вкладки '''Verifier''' при каком-нибудь выделенном свойстве завершает вывод словами '''Property is satisfied''' или '''Property is not satisfied'''.
−
** для выполнения задания "Spin" в паре: '''[ver-spin] группа Фамилия И.О., Фамилия И.О.'''
+
−
** для выполнения задания "Uppaal" в одиночку: '''[ver-uppaal] группа Фамилия И.О.'''
+
−
** для выполнения задания "Uppaal" в паре: '''[ver-uppaal] группа Фамилия И.О., Фамилия И.О.'''
+
−
* В ответ будет выслано письмо, содержащее описание системы и цели исследования этой системы при помощи проверки требований.
+
−
* В тексте первого письма можно сформулировать пожелания по виду системы и целей исследования, вплоть до полной формулировки:
+
−
** если пожелания разумны, они с немалой вероятностью будут учтены в задании;
+
−
** типовые примеры пожеланий: "хочу исследовать параллельно работающие программы", "... схему", "... игру/головоломку", "... систему общего вида, без программистско-математической специализации".
+
−
* Решение задания должно быть выслано в ответ на письмо с формулировкой задания в установленный срок.
+
−
* Присланное решение
+
−
** принимается, если оно полностью или с незначительными недочётами верно;
+
−
** не принимается, если оно демонстрирует, что выполнявшие его не пытались вдумчиво разобраться в принципах работы со средством верификации;
+
−
** отправляется на доработку, если оно содержит существенные ошибки, но демонстрирует осознанную и в немалой степени правильную работу со средством верификации.
+
  
−
== NuSMV ==
+
Для полноценной работы на семинарах, посвящённых средствам верификации, требуется принести и использовать свой ноутбук (или хотя бы ноутбук соседа).
 +
Участие без ноутбука тоже возможно: слушать, смотреть, записывать, но без возможности воспроизвести обсуждаемое или попробовать что-то своё.
  
−
Решение этого задания - это
+
== Общие правила выполнения заданий "Spin", "NuSMV", "Uppaal" ==
−
* файл с расширением ".smv", содержащий формализацию системы и требований в формате средства NuSMV, и
+
 
−
* пояснение того, как результаты проверки требований, выдаваемые NuSMV, соотносятся с поставленными целями, в свободной форме.
+
Задания можно выполнять в одиночку или вдвоём.
 +
Для получения задания следует отправить [[Подымов Владислав Васильевич|ему]] на почту письмо с любым текстом и заголовком в следующем формате ('''ZZ''' заменяется на '''spin''', '''nusmv''' или '''uppaal''' в зависимости от того, какое задание запрашивается):
 +
* '''[ver-ZZ] группа Фамилия И.О.''' для выполнения в одиночку.
 +
* '''[ver-ZZ] группа Фамилия И.О., Фамилия И.О.''' для выполнения вдвоём.
 +
В ответ будет выслано письмо с системой и целями её исследования при помощи проверки требований.
 +
 
 +
В тексте письма можно выразить пожелания о том, какого рода задание хочется, вплоть до точной формулировки.
 +
Разумные пожелания будут учтены по возможности.
 +
Типовые примеры пожеланий: примеры пожеланий: "хочу исследовать параллельно работающие программы", "... схему", "... игру/головоломку", "... систему общего вида, без программистско-математической специализации".
 +
 
 +
Срок выполнения заданий:
 +
* Первый дедлайн указан в плане занятий. Если все задачи сданы к своим первым дедлайнам, то (помимо отсутствия штрафов за невыполнение заданий) выдаётся некоторое поощрение.
 +
* Второй дедлайн - конец семестра (20 декабря). Если все задачи сданы в этот срок, то выдаётся чуть меньшее поощрение.
 +
* Третий дедлайн - вплоть до экзамена, пока лектору не надоест. Имейте в виду, что задание, присланное слишком близко к экзамену, может быть и не проверено, если лектору надоело.
 +
 
 +
Присланное решение принимается, не принимается или отправляется на доработку в зависимости от того, насколько оно правильно и, если есть ошибки, насколько хорошо в нём видны осознанные попытки разобраться в принципах работы со средством верификации.
  
 
== Spin ==
 
== Spin ==
Строка 153: Строка 214:
 
Решение этого задания - это
 
Решение этого задания - это
 
* файл с расширением ".pml", содержащий формализацию системы и требований на языке PROMELA, и
 
* файл с расширением ".pml", содержащий формализацию системы и требований на языке PROMELA, и
−
* пояснение того, как результаты проверки требований, выдаваемые средством Spin, соотносятся с поставленными целями, в свободной форме.
+
* пояснение в свободной форме того, как результаты проверки требований, выдаваемые средством Spin, соотносятся с поставленными целями.
 +
 
 +
== NuSMV ==
 +
 
 +
Решение этого задания - это
 +
* файл с расширением ".smv", содержащий формализацию системы и требований в формате средства NuSMV, и
 +
* пояснение в свободной форме того, как результаты проверки требований, выдаваемые NuSMV, соотносятся с поставленными целями.
  
 
== Uppaal ==
 
== Uppaal ==
Строка 159: Строка 226:
 
Решение этого задания - это
 
Решение этого задания - это
 
* файл или файлы, сгенерированные средством Uppaal и содержащие формализацию системы и требований (Uppaal 4.1: файл ".xml"; Uppaal 4.0: файлы ".xml" и ".q"), и
 
* файл или файлы, сгенерированные средством Uppaal и содержащие формализацию системы и требований (Uppaal 4.1: файл ".xml"; Uppaal 4.0: файлы ".xml" и ".q"), и
−
* пояснение того, как результаты проверки требований, выдаваемые средством Uppaal, соотносятся с поставленными целями, в свободной форме.
+
* пояснение в свободной форме того, как результаты проверки требований, выдаваемые средством Uppaal.
  
 
= Премиальные задачи =
 
= Премиальные задачи =
Строка 178: Строка 245:
  
 
Если написать письмо с любым содержанием и заголовком '''[ver-ctl] группа Фамилия И.О.''', то в ответ будут присланы описание системы и требований к этой системе.
 
Если написать письмо с любым содержанием и заголовком '''[ver-ctl] группа Фамилия И.О.''', то в ответ будут присланы описание системы и требований к этой системе.
−
Требуется адекватно формализовать требования в логике ветвящегося времени и изобразить шаги работы табличного или символьного алгоритма.
+
Требуется адекватно формализовать требования в логике ветвящегося времени и изобразить шаги работы базового или символьного алгоритма.
  
 
Если сомневаетесь, что означает "изобразить шаги работы алгоритма", то по умолчанию поступайте так:
 
Если сомневаетесь, что означает "изобразить шаги работы алгоритма", то по умолчанию поступайте так:
−
* табличный алгоритм:
+
* базовый алгоритм:
 
** нарисовать модель Крипке, адекватно описывающую систему;
 
** нарисовать модель Крипке, адекватно описывающую систему;
−
** описать пошаговое получение разметки алгоритмом настолько (''не'')строго, чтобы можно было без чрезмерных усилий строго восстановить каждый шаг работы алгоритма;
+
** описать пошаговое получение информации о выполнимости подформул алгоритмом настолько (''не'')строго, чтобы можно было без чрезмерных усилий строго восстановить каждый шаг работы алгоритма;
 
* символьный алгоритм:
 
* символьный алгоритм:
−
** описать модель Крипке в символьной записи (основанной на любом общеизвестном представлении булевых функций);
+
** описать символьное представление модели Крипке (основанной на любом общеизвестном представлении булевых функций);
 
** описать пошаговое преобразование символьных записей алгоритмом настолько (''не'')строго, чтобы можно было без чрезмерных усилий строго восстановить каждый шаг работы алгоритма.
 
** описать пошаговое преобразование символьных записей алгоритмом настолько (''не'')строго, чтобы можно было без чрезмерных усилий строго восстановить каждый шаг работы алгоритма.
  
Строка 212: Строка 279:
 
#Baier C., Katoen J.-P. Principles of model checking, MIT Press, 2008.  
 
#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.
 
#Clarke E., Henzinger T.A., Veith H., Bloem R. Handbook of model checking, Springer, 2018.
−
 
−
= Прошлогодние лекции =
 
−
 
−
Видеозаписи лекций размещены по адресу [https://m.cs.msu.ru/index.php/s/N6FkcmFbxQkS8z9] в разделе '''ЗахаровВА'''
 
−
 
−
#Verification problem for hardware and software systems. Why do we need formal verification of information processing systems? Basic approaches to formal verification of hardware and software systems. Principles of model checking. Historical overview. Achievements of formal verification techniques. '''[[Media: Lecture_Verification_1.pdf| Лекция 1.]]'''
 
−
<!-- '''[[Media: Lecture_Verification_1.pdf| Лекция 1.]]''' -->
 
−
#General principles of deductive program verification. Operational semantics of imperative programs. Problem statement for deductive verification of imperative programs. Hoare logic: theory and practice. Automation of program correctness checking. '''[[Media: Lecture_Verification_2.pdf| Лекция 2.]]'''
 
−
<!-- '''[[Media: Lecture_Verification_2.pdf| Лекция 2.]]''' -->
 
−
#General principles of model checking. Kripke structures as formal models of information processing systems. First-order representation of Kripke structures. Synchronous and asynchronous models. Granularity of models. Translation of programs into Kripke structure. '''[[Media: Lecture_Verification_3.pdf| Лекция 3.]]'''
 
−
#Properties of program computations. Classification of computational properties. Fairness constraints. Generalized Computational Tree Logic CTL*: syntax and semantics. Temporal Logics CTL and LTL. Formal setting of model checking problem. '''[[Media: Lecture_Verification_4.pdf| Лекция 4.]]'''
 
−
#Tableau-based model checking for CTL. Correctness and complexity of CTL model checking. “Combinatorial explosion” problem. Symbolic representation of formal models. Binary Decision Diagrams (BDDs). Reduction of BDDs to canonical forms (ROBDDs). Operations on ROBDDs: unary and binary Boolean operations, quantification, satisfiability checking. '''[[Media: Lecture_Verification_5.pdf| Лекция 5.]]'''
 
−
#Basics of Fixed Point Theory. Fixed point characterization of CTL temporal operators. Symbolic model checking algorithm for CTL. '''[[Media: Lecture_Verification_6.pdf| Лекция 6.]]'''
 
−
#Model checking problem for LTL. Model checking algorithms for LTL: tableau-based, automata-based. Büchi automata: basic properties and generalizations. '''[[Media: Lecture_Verification_7.pdf| Лекция 7.]]'''
 
−
<!-- #Особенности параллельных вычислений асинхронных распределенных систем. Независимость действий. Проскальзывающие действия. Достаточные множества переходов и их свойства. Вычисление достаточных множеств переходов. Статическая и динамическая редукция частичных порядков на основе достаточных множеств переходов. <!--'''[[Media: Lecture_Verification_8.pdf| Лекция 8.]]''' -->
 
−
# Bisimulation and simulation for Kripke models. Computing bisimulation relation for Kripke models. Bisimulation and simulation reduction of Kripke models. Reduction of Kripke models by the influence cones. Data abstraction techniques. '''[[Media: Lecture_Verification_8.pdf| Лекция 8.]]'''
 
−
#Real-time systems. Timed automata (TA). Infeasible runs of TA. Timed computational tree logic (TCTL). Model checking problem for TCTL. '''[[Media: Lecture_Verification_9.pdf| Лекция 9.]]'''
 
−
#A model-checking algorithm for TCTL. Clock and state regions. Region transition systems. Networks of timed automata. '''[[Media: Lecture_Verification_10.pdf| Лекция 10.]]'''
 
−
#Bounded model checking (BMC). Reduction of BMC to thr Satisfiability Chercking Problem (SAT). Application of SAT solvers to BMC problem. '''[[Media: Lecture_Verification_11.pdf| Лекция 11.]]'''
 

Текущая версия на 12:55, 27 ноября 2025

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

Обязательный курс для магистров групп 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. Символьный алгоритм model checking для CTL (начало).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Семинары

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

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

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

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

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

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

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

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

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

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

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

Экзамен

Экзамен проводится письменно, длительность - 120 минут. Экзаменационная работа состоит из следующих задач:

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

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

Каждая экзаменационная задача оценивается по шкале от 0 до 4 баллов. Эти баллы суммируются, и к ним прибавляются баллы за премиальные задачи. Оценка за экзамен зависит от суммарного балла и от сдачи обязательных заданий так:

Количество зачтённых обязательных заданий
3 2 1 или 0
Баллы 29 или больше Отлично Хорошо Удовлетворительно
22-28 Хорошо Удовлетворительно Неудовлетворительно
15-21 Удовлетворительно Неудовлетворительно Неудовлетворительно
меньше 15 Неудовлетворительно Неудовлетворительно Неудовлетворительно

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

Курсом предполагаются три обязательных домашних задания: "Spin", "NuSMV", "Uppaal".

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

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

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

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

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

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

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

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

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

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

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

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

  • Первый дедлайн указан в плане занятий. Если все задачи сданы к своим первым дедлайнам, то (помимо отсутствия штрафов за невыполнение заданий) выдаётся некоторое поощрение.
  • Второй дедлайн - конец семестра (20 декабря). Если все задачи сданы в этот срок, то выдаётся чуть меньшее поощрение.
  • Третий дедлайн - вплоть до экзамена, пока лектору не надоест. Имейте в виду, что задание, присланное слишком близко к экзамену, может быть и не проверено, если лектору надоело.

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

Spin

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

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

NuSMV

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

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

Uppaal

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

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

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

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

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

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

Логика Хоара

Задание сформулировано на последнем слайде материалов семинара 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=12374»