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

Материал из Кафедра математической кибернетики
Перейти к: навигация, поиск
 
(не показаны 63 промежуточных версий 2 участников)
Строка 1: Строка 1:
= Общая информация =
+
[[Категория:Лекционные курсы кафедры МК]]
 +
[[Категория:Магистерская программа Дискретные управляющие системы и их приложения]]
 +
''Актуальность информации: осенний семестр 2023/2024 учебного года.''
  
 +
Обязательный курс для магистров групп 618мк_дс, 618мк_дус и 621асвк 3 семестра магистратуры (группа 621асвк - "Методы верификации программ").
 +
Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].
  
Обязательный курс для магистров 618/2 и 621 групп 3 семестра магистратуры (группа 621 - "Методы верификации программ").
+
= Лекции =
  
В 2018-2019 учебном году курс читают
+
[[Media: Verif_VP_01.pdf|Блок 1]] (вводный). Что такое и зачем нужна формальная верификация.
  
* профессор [[Захаров Владимир Анатольевич|В. А. Захаров]]
+
[[Media: Verif_VP_02.pdf|Блок 2.]] Логика предикатов (напоминание).
* научный сотрудник [[Подымов Владислав Васильевич|В. В. Подымов]].
+
  
<!-- Лекционная нагрузка — 32 ч., семинары и практические занятия— 16 ч. -->
+
[[Media: Verif_VP_03.pdf|Блок 3.]] Общие принципы дедуктивной верификации программ. Модельные императивные программы: синтаксис, операционная семантика.
  
= Программа =
+
[[Media: Verif_VP_04.pdf|Блок 4.]] Дедуктивная верификация программ: постановка задачи, логика Хоара.
  
''Программа будет обновляться по мере проведения занятий.''
+
[[Media: Verif_VP_05.pdf|Блок 5.]] Дедуктивная верификация программ: аннотированные программы.
  
#Задача верификации аппаратуры и программного обеспечения. Зачем нужна формальная верификация программ? Основные подходы к задаче формальной верификации. Принципы верификации моделей программ. Исторические сведения. Достижения методов формальной верификации программ. Алгоритмические и комбинаторные трудности применения метода верификации моделей программ. '''[[Media: Lecture_Verification_1.pdf| Лекция 1.]]'''
+
[[Media: Verif_VP_06.pdf|Блок 6.]] Дедуктивная верификация программ: возможности автоматизации, слабейшее предусловие.
#Общие принципы дедуктивной верификации программ. Операционная семантика императивных программ. Формальная постановка задачи верификации программ. Логика Хоара: правила вывода и свойства. Аннотированные программы. Автоматизация проверки правильности программ. '''[[Media: Lecture_Verification_2.pdf| Лекция 2.]]'''
+
#Моделирование схем. Системы переходов - модели Крипке. Представление систем переходов формулами логики предикатов первого порядка. Синхронные и асинхронные схемы. Степень детализации представления. Трансляция описаний программ и схем в модели Крипке. '''[[Media: Lecture_Verification_3.pdf| Лекция 3.]]'''
+
#Темпоральная логика деревьев вычислений CTL. Синтаксис и семантика CTL. Примеры спецификаций моделей в терминах формул CTL. Темпоральная логика линейного времени LTL. Синтаксис и семантика LTL. Свойства живости и безопасности. Ограничения справедливости. Задача верификации моделей (model-checking). '''[[Media: Lecture_Verification_4.pdf| Лекция 4.]]'''
+
#Табличный алгоритм верификации моделей для CTL. Обоснование корректности и сложности табличного алгоритма верификации моделей. Проблема “комбинаторного взрыва”. Символьные средства описания моделей. Двоичные разрешающие диаграммы (BDD). Алгоритм редукции BDD к каноническому виду (OBDD). Выполнение операций над OBDD: унарные и бинарные булевы операции, квантификация, проверка выполнимости, подсчет числа единиц. Общие представления о сложности в классе OBDD. '''[[Media: Lecture_Verification_5.pdf| Лекция 5.]]'''
+
#Представления неподвижной точки в CTL. Алгоритм символьной верификации моделей в CTL. '''[[Media: Lecture_Verification_6.pdf| Лекция 6.]]'''
+
#Табличный алгоритм верификации моделей для LTL. Автоматы Бюхи, их свойства и обобщения. Трансляция моделей Крипке и формул LTL в автоматы Бюхи. Автоматный алгоритм верификации моделей для LTL. '''[[Media: Lecture_Verification_7.pdf| Лекция 7.]]'''
+
<!-- #Особенности параллельных вычислений асинхронных распределенных систем. Независимость действий. Проскальзывающие действия. Достаточные множества переходов и их свойства. Вычисление достаточных множеств переходов. Статическая и динамическая редукция частичных порядков на основе достаточных множеств переходов. <!--'''[[Media: Lecture_Verification_8.pdf| Лекция 8.]]''' -->
+
#Отношения бисимуляционной эквивалентности (бисимуляции) и симуляционного квазипорядка (симуляции) на моделях Крипке. Равновыполнимость темпоральных формул на бисимуляционно эквивалентных моделях Крипке. Вычисление классов бисимуляционной эквивалентности на конечных моделях Крипке. Упрощение моделей Крипке при помощи отношений симуляции и и бисимуляции. Редукция моделей Крипке по конусу влияния. Абстракции данных при построении моделей Крипке. '''[[Media: Lecture_Verification_8.pdf| Лекция 8.]]'''
+
#Системы реального времени. Временные автоматы. Неправдоподобные вычисления временных автоматов. Вычисления Зенона. Timed CTL. Задача model checking для Timed CTL. '''[[Media: Lecture_Verification_9.pdf| Лекция 9.]]'''
+
#Алгоритм верификации временных автоматов относительно Timed CTL. Временные регионы. Оценка числа регионов. Системы регионов. Сети временных автоматов. '''[[Media: Lecture_Verification_10.pdf| Лекция 10.]]'''
+
#Верификация моделей программ для вычислений ограниченной длины (bounded model checking, BMC). Сведение задачи BMC к задаче проверки выполнимости булевых формул (SAT). Применение автоматических средств решения задачи SAT для решения задачи BMC. <!--'''[[Media: Lecture_Verification_11.pdf| Лекция 11.]]'''-->
+
  
= Материалы семинаров =
+
[[Media: Verif_VP_07.pdf|Блок 7.]] Общая схема метода model checking.
  
''Материалы будут обновляться по мере проведения занятий.''
+
[[Media: Verif_VP_08.pdf|Блок 8.]] Модели Крипке.
  
'''Любые''' вопросы по темам семинарских занятий можно задавать [[Подымов Владислав Васильевич|ему]].
+
[[Media: Verif_VP_09.pdf|Блок 9.]] Особенности моделирования систем.
  
'''[[Media: Seminar_Verification_1.pdf| Семинар 1.]]''' Обоснование корректности программ при помощи логики Хоара.
+
[[Media: Verif_VP_10.pdf|Блок 10.]] Пара слов о последовательностях.
  
'''[[Media: Seminar_Verification_2.pdf| Семинар 2.]]''' Модели Крипке. LTL. Безопасность, живость.
+
[[Media: Verif_VP_11.pdf|Блок 11.]] Свойства трасс. Безопасность и живость.
  
'''[[Media: Seminar_Verification_3.pdf| Семинар 3.]]''' Справедливость. CTL: формализация, табличный и символьный алгоритмы. ROBDD.
+
[[Media: Verif_VP_12.pdf|Блок 12.]] Логика линейного времени (LTL). Постановка задачи верификации моделей Крипке относительно LTL.
  
'''[[Media: Seminar_Verification_4.pdf| Семинар 4.]]''' NuSMV: обзор средства.
+
[[Media: Verif_VP_13.pdf|Блок 13.]] Размеченные системы переходов. Справедливость для систем переходов. Справедливость в LTL.
  
'''[[Media: Seminar_Verification_5.pdf| Семинар 5-6.]]''' NuSMV: практические задания по проверке CTL-спецификаций.
+
[[Media: Verif_VP_14.pdf|Блок 14.]] Автоматный алгоритм model checking для LTL: общая схема.
  
'''[[Media: Seminar_Verification_7.pdf| Семинар 7.]]''' Обзор средства SPIN: синтаксис, трансляция базовых конструкций в модели Крипке.
+
[[Media: Verif_VP_15.pdf|Блок 15.]] Автоматы Бюхи. Обобщённые автоматы Бюхи.
  
'''[[Media: Seminar_Verification_7_spin_manual.pdf| Инструкция по работе со средством SPIN.]]'''
+
[[Media: Verif_VP_16.pdf|Блок 16.]] Пересечение автоматов Бюхи.
  
'''[[Media: Seminar_Verification_8.pdf| Семинар 8-9.]]''' SPIN: практические задания по проверке LTL-спецификаций.
+
[[Media: Verif_VP_17.pdf|Блок 17.]] Проверка пустоты автомата Бюхи.
  
'''[[Media: Seminar_Verification_10.pdf| Семинар 10-11.]]''' UPPAAL: практические задания по проверке TCTL-спецификаций.
+
[[Media: Verif_VP_18.pdf|Блок 18.]] Автоматы Бюхи для моделей Крипке
  
'''[[Media: Seminar_Verification_10_errors.zip| Архив, прилагающийся к семинару 10-11.]]
+
[[Media: Verif_VP_19.pdf|Блок 19.]] Автоматы Бюхи для ltl-формул.
  
= Правила проведения экзамена =
+
[[Media: Verif_VP_20.pdf|Блок 20.]] Автоматный алгоритм model checking для LTL: уточнённая схема.
  
# Итоговая экзаменационная оценка складывается из оценки за экзаменационную контрольную работу, зачетных оценок за выполнение домашних заданий и премиальных оценок за решение особо сложных задач, объявленных в курсе лекций.
+
[[Media: Verif_VP_21.pdf|Блок 21.]] Логика деревьев вычислений (CTL). Постановка задачи верификации моделей Крипке относительно CTL.
# Экзаменационная контрольная работа состоит из 5 задач и 5 вопросов. Каждая из задач контрольной относится к одному из типов задач, которые разбирались на семинарских занятиях или на лекциях. Каждый из вопросов касается формулировок определений или ключевых результатов, рассмотренных на лекциях.
+
  
== Учет домашних заданий ==
+
[[Media: Verif_VP_22.pdf|Блок 22.]] Базовый алгоритм model checking для CTL.
  
'''Логика Хоара:''' выполнившие это задание освобождаются от решения задачи на тему логики Хоара, и за особые заслуги могут быть поощрены дополнительной премиальной оценкой.
+
[[Media: Verif_VP_23.pdf|Блок 23.]] Справедливость и CTL.
  
'''CTL: формализация требований и алгоритмы проверки формул:''' выполнившие это задание освобождаются от задач, покрываемых темами заданий, и могут быть поощрены дополнительной премиальной оценкой за особые заслуги (например, демонстрацию хорошего понимания устройства символьного алгоритма).
+
[[Media: Verif_VP_24.pdf|Блок 24.]] Символьные представления моделей.
  
'''CTL и справедливость:''' этим заданием покрывается часть задания "алгоритм верификации CTL-формул", и кроме того, выполнившие это задание будут поощрены дополнительной премиальной оценкой.
+
[[Media: Verif_VP_25.pdf|Блок 25.]] Двоичные решающие диаграммы: BDD, OBDD, ROBDD.
  
'''NuSMV, Spin, Uppaal:'''
+
[[Media: Verif_VP_26.pdf|Блок 26.]] Символьный алгоритм model checking для CTL (начало).
* если выполнены ровно два из трёх заданий, то из итоговой экзаменационной оценки (''2'', ''3'', ''4'', ''5'') вычитается один балл;
+
* если выполнено менее двух заданий, то из итоговой экзаменационной оценки вычитается два балла.
+
  
= Обязательные домашние задания "NuSMV", "Spin", "Uppaal" =
+
[[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.
 +
 
 +
= Обязательные домашние задания =
 +
 
 +
Курсом предполагаются три обязательных домашних задания: "NuSMV", "Spin" и "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.]]
  
 
== Установка средств верификации ==
 
== Установка средств верификации ==
Строка 106: Строка 158:
 
** принимается, если оно полностью или с незначительными недочётами верно;
 
** принимается, если оно полностью или с незначительными недочётами верно;
 
** не принимается, если оно демонстрирует, что выполнявшие его не пытались вдумчиво разобраться в принципах работы со средством верификации;
 
** не принимается, если оно демонстрирует, что выполнявшие его не пытались вдумчиво разобраться в принципах работы со средством верификации;
** отправляется на доработку, если оно содержит существенные ошибки, но демонстрирует осознанную и правильную работу со средством верификации.
+
** отправляется на доработку, если оно содержит существенные ошибки, но демонстрирует осознанную и в немалой степени правильную работу со средством верификации.
  
 
== NuSMV ==
 
== NuSMV ==
Строка 126: Строка 178:
 
* пояснение того, как результаты проверки требований, выдаваемые средством Uppaal, соотносятся с поставленными целями, в свободной форме.
 
* пояснение того, как результаты проверки требований, выдаваемые средством Uppaal, соотносятся с поставленными целями, в свободной форме.
  
= Поощряемые домашние задания =
+
= Правила проведения экзамена =
  
Решение домашних заданий, а также ''любые'' вопросы по домашним заданиям можно высылать на почту [[Подымов Владислав Васильевич|ему]].
+
Итоговая экзаменационная оценка складывается из
 +
* оценки за экзаменационную контрольную работу,
 +
* зачетных оценок за выполнение [[#Обязательные домашние задания|обязательных домашних заданий]] и
 +
* оценок за решение [[#Премиальные задачи|премиальных задач]].
  
== Логика Хоара ==
+
Экзаменационная контрольная работа проводится письменно, длительность - 150 минут, и состоит из 5 практических и 5 теоретических задач.
 +
Каждая из практических задач относится к одному из типов, которые разбирались на семинарах или в лекциях.
 +
Каждая из теоретических задач касается формулировок определений или ключевых результатов, рассмотренных в лекциях.
  
Крайний срок выполнения задания: начало семинара 3 (по CTL).
+
= Премиальные задачи =
 +
 
 +
Крайний срок выполнения всех премиальных задач - конец семестра.
 +
 
 +
== Лекционные премиальные задачи ==
 +
 
 +
Эти задачи явно обозначаются в слайдах лекций.
 +
 
 +
== Логика Хоара ==
  
 
Задание сформулировано на последнем слайде материалов семинара 1.
 
Задание сформулировано на последнем слайде материалов семинара 1.
 +
 +
Выполнившие это задание освобождаются от решения задачи на тему логики Хоара на экзамене и могут быть поощрены дополнительно за особые заслуги.
  
 
== CTL: формализация требований и алгоритмы проверки формул ==
 
== CTL: формализация требований и алгоритмы проверки формул ==
  
Крайний срок выполнения задания: конец семестра.
+
Если написать письмо с любым содержанием и заголовком '''[ver-ctl] группа Фамилия И.О.''', то в ответ будут присланы описание системы и требований к этой системе.
 
+
Требуется адекватно формализовать требования в логике ветвящегося времени и изобразить шаги работы базового или символьного алгоритма.
Как выполнить это задание:
+
* написать письмо с любым содержанием и заголовком '''[ver-ctl] группа Фамилия И.О.''';
+
* в ответ будут присланы описание системы и требований к этой системе;
+
* требуется адекватно формализовать требования в логике ветвящегося времени, изобразить шаги работы табличного или символьного алгоритма и донести результат до [[Подымов Владислав Васильевич|него]] в любом виде.
+
  
 
Если сомневаетесь, что означает "изобразить шаги работы алгоритма", то по умолчанию поступайте так:
 
Если сомневаетесь, что означает "изобразить шаги работы алгоритма", то по умолчанию поступайте так:
* табличный алгоритм:
+
* базовый алгоритм:
 
** нарисовать модель Крипке, адекватно описывающую систему;
 
** нарисовать модель Крипке, адекватно описывающую систему;
** описать пошаговое получение разметки алгоритмом настолько (''не'')строго, чтобы можно было без чрезмерных усилий строго восстановить каждый шаг работы алгоритма;
+
** описать пошаговое получение информации о выполнимости подформул алгоритмом настолько (''не'')строго, чтобы можно было без чрезмерных усилий строго восстановить каждый шаг работы алгоритма;
 
* символьный алгоритм:
 
* символьный алгоритм:
** описать модель Крипке в символьной записи (основанной на любом общеизвестном представлении булевых функций);
+
** описать символьное представление модели Крипке (основанной на любом общеизвестном представлении булевых функций);
 
** описать пошаговое преобразование символьных записей алгоритмом настолько (''не'')строго, чтобы можно было без чрезмерных усилий строго восстановить каждый шаг работы алгоритма.
 
** описать пошаговое преобразование символьных записей алгоритмом настолько (''не'')строго, чтобы можно было без чрезмерных усилий строго восстановить каждый шаг работы алгоритма.
 +
 +
Выполнившие это задание освобождаются от задач, темы которых покрываются этим заданием, и могут быть поощрены дополнительно за особые заслуги (например, за хорошее понимание устройства символьного алгоритма).
  
 
== CTL и справедливость ==
 
== CTL и справедливость ==
  
 
Это '''трудное''' домашнее задание.
 
Это '''трудное''' домашнее задание.
 
Крайний срок выполнения задания: конец семестра.
 
  
 
При выполнении этого задания автоматически засчитывается часть задания "CTL: формализация требований и алгоритмы проверки формул", относящаяся к изображению шагов работы алгоритма.
 
При выполнении этого задания автоматически засчитывается часть задания "CTL: формализация требований и алгоритмы проверки формул", относящаяся к изображению шагов работы алгоритма.
  
Как выполнить это задание:
+
Требуется:
 
* предложить описание символьного алгоритма верификации CTL-формул, работающего в условиях справедливости для CTL:
 
* предложить описание символьного алгоритма верификации CTL-формул, работающего в условиях справедливости для CTL:
 
** можно написать псевдокод с пояснениями,
 
** можно написать псевдокод с пояснениями,
Строка 167: Строка 230:
 
** можно написать программу,
 
** можно написать программу,
 
** ...;
 
** ...;
* привести пример работы алгоритма, иллюстрирующий его отличие от "несправедливого" символьного алгоритма;
+
* привести пример работы алгоритма, иллюстрирующий его отличие от "несправедливого" символьного алгоритма.
* донести результаты выполнения задания до руководителей курса в любом виде.
+
  
 
= Литература =
 
= Литература =
Строка 177: Строка 239:
 
#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.
 
#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.  
 
#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.
 
+
[[Категория:Лекционные курсы кафедры МК]]
+
[[Категория:Магистерская программа Дискретные управляющие системы и их приложения]]
+

Текущая версия на 11:02, 22 января 2024

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  • Каждое из заданий можно выполнять как в одиночку, так и в паре.
  • Срок выполнения задания (кроме индивидуально согласованных случаев) - от начала проведения соответствующих семинаров и до начала проведения следующего тематического блока семинаров (для последнего блока семинаров - до окончания семестра).
  • Первый шаг выполнения - выслать ему на почту письмо с любым текстом и специальным заголовком:
    • для выполнения задания "NuSMV" в одиночку: [ver-nusmv] группа Фамилия И.О.
    • для выполнения задания "NuSMV" в паре: [ver-nusmv] группа Фамилия И.О., Фамилия И.О.
    • для выполнения задания "Spin" в одиночку: [ver-spin] группа Фамилия И.О.
    • для выполнения задания "Spin" в паре: [ver-spin] группа Фамилия И.О., Фамилия И.О.
    • для выполнения задания "Uppaal" в одиночку: [ver-uppaal] группа Фамилия И.О.
    • для выполнения задания "Uppaal" в паре: [ver-uppaal] группа Фамилия И.О., Фамилия И.О.
  • В ответ будет выслано письмо, содержащее описание системы и цели исследования этой системы при помощи проверки требований.
  • В тексте первого письма можно сформулировать пожелания по виду системы и целей исследования, вплоть до полной формулировки:
    • если пожелания разумны, они с немалой вероятностью будут учтены в задании;
    • типовые примеры пожеланий: "хочу исследовать параллельно работающие программы", "... схему", "... игру/головоломку", "... систему общего вида, без программистско-математической специализации".
  • Решение задания должно быть выслано в ответ на письмо с формулировкой задания в установленный срок.
  • Присланное решение
    • принимается, если оно полностью или с незначительными недочётами верно;
    • не принимается, если оно демонстрирует, что выполнявшие его не пытались вдумчиво разобраться в принципах работы со средством верификации;
    • отправляется на доработку, если оно содержит существенные ошибки, но демонстрирует осознанную и в немалой степени правильную работу со средством верификации.

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.