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

Материал из Кафедра математической кибернетики
Перейти к: навигация, поиск
 
(не показаны 114 промежуточные версии 2 участников)
Строка 1: Строка 1:
−
= '''[[Media: ExamVerification-2016.pdf|РЕЗУЛЬТАТЫ ЭКЗАМЕНА 14.01.2016]]''' =
+
[[Категория:Спецкурсы кафедры МК]]
 +
[[Категория:Лекционные курсы кафедры МК]]
 +
[[Категория:Магистерская программа Дискретные управляющие системы и их приложения]]
 +
''Актуальность информации: осенний семестр 2024/2025 учебного года.''
  
−
= Общая информация =
+
Обязательный курс для магистров групп 618мк_дса, 618мк_дус и 621асвк 3 семестра магистратуры (группа 621асвк - "Методы верификации программ").
 +
Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].
  
 +
= Лекции =
  
−
Обязательный курс для магистров 618 и 621 группы 11 семестра обучения.  
+
[[Media: Verif_VP_01.pdf|Блок 1]] (вводный). Что такое и зачем нужна формальная верификация.
  
−
Курс читают
+
[[Media: Verif_VP_02.pdf|Блок 2.]] Логика предикатов (напоминание).
  
−
* профессор [[Захаров Владимир Анатольевич|В. А. Захаров]]
+
[[Media: Verif_VP_03.pdf|Блок 3.]] Общие принципы дедуктивной верификации программ. Модельные императивные программы: синтаксис, операционная семантика.
−
* младший научный сотрудник [[Подымов Владислав Васильевич|В. В. Подымов]].
+
  
−
Лекционная нагрузка — 32 ч., семинары и практические занятия— 16 ч.
+
[[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. Темпоральная логика линейного времени PLTL. Синтаксис и семантика PLTL. Свойства живости и безопасности. Ограничения справедливости. Задача верификации моделей (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.]]'''
+
−
#Табличная верификация моделей для PLTL. Автоматы Бюхи: их свойства и обобщения. Трансляция формул PLTL в автоматы Бюхи. Сведение задачи проверки выполнимости формул PLTL к проблеме пустоты для автоматов Бюхи. <!-- Алгоритм двойного поиска в глубину с возвратом (DDFS) для проверки пустоты автоматов Бюхи. --> '''[[Media: Lecture_Verification_7.pdf| Лекция 7.]]'''
+
−
<!-- #Особенности параллельных вычислений асинхронных распределенных систем. Независимость действий. Проскальзывающие действия. Достаточные множества переходов и их свойства. Вычисление достаточных множеств переходов. Статическая и динамическая редукция частичных порядков на основе достаточных множеств переходов. '''[[Media: Lecture_Verification_8.pdf| Лекция 8.]]''' -->
+
−
#Отношения бисимуляционной эквивалентности (бисимуляции) и симуляционного квазипорядка (симуляции) на моделях Крипке. Равновыполнимость темпоральных формул на бисимуляционно эквивалентных моделях Крипке. Вычисление классов бисимуляционной эквивалентности на конечных моделях Крипке. Упрощение моделей Крипке при помощи отношений симуляции и и бисимуляции. Редукция моделей Крипке по конусу влияния. Абстракции данных при построении моделей Крипке. '''[[Media: Lecture_Verification_8.pdf| Лекция 8.]]'''
+
−
#Временные автоматы как формальные модели распределенных систем реального времени. Вычисления временных автоматов. Примеры использования временных автоматов для моделирования встроенных систем. Зеноновские вычисления. Синтаксис и семантика Timed CTL. Примеры формальных спецификаций поведения встроенных систем при помощи TCTL. '''[[Media: Lecture_Verification_9.pdf| Лекция 9.]]'''
+
−
#Задача верификации моделей программ реального времени. Отношение эквивалентности часов и регионы. Регионные системы переходов. Оценка числа регионов. Сведение задачи верификации временных автоматов относительно TCTL к задаче верификации моделей Крипке относительно 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.
  
−
''Любые'' вопросы по темам семинарских занятий можно высылать на почту [[Подымов Владислав Васильевич| valdus@yandex.ru]].
+
[[Media: Verif_VP_08.pdf|Блок 8.]] Модели Крипке.
  
−
'''[[Media: Seminar_Verification_1.pdf| Семинар 1.]]''' Доказательство корректности императивных программ с помощью логики Хоара.
+
[[Media: Verif_VP_09.pdf|Блок 9.]] Особенности моделирования систем.
  
−
'''[[Media: Seminar_Verification_2.pdf| Семинар 2.]]''' Модели Крипке. LTL, CTL. Безопасность, живость, справедливость.
+
[[Media: Verif_VP_10.pdf|Блок 10.]] Пара слов о последовательностях.
  
−
'''[[Media: Seminar_Verification_3.pdf| Семинар 3.]]''' Табличный и символьный алгоритмы проверки CTL-формул на моделях Крипке. ROBDD.
+
[[Media: Verif_VP_11.pdf|Блок 11.]] Свойства трасс. Безопасность и живость.
  
−
'''[[Media: Seminar_Verification_4.pdf| Семинар 4.]]''' Обзор средства NuSMV: описание параллельной композиции автоматов, проверка CTL-формул.
+
[[Media: Verif_VP_12.pdf|Блок 12.]] Логика линейного времени (LTL). Постановка задачи верификации моделей Крипке относительно LTL.
  
−
'''[[Media: Seminar_Verification_5.pdf| Семинар 5-6.]]''' NuSMV: практические задания по проверке CTL-спецификаций.
+
[[Media: Verif_VP_13.pdf|Блок 13.]] Размеченные системы переходов. Справедливость для систем переходов. Справедливость в LTL.
  
−
'''[[Media: Seminar_Verification_7.pdf| Семинар 7.]]''' Обзор средства SPIN: синтаксис, трансляция базовых конструкций в модели Крипке.
+
[[Media: Verif_VP_14.pdf|Блок 14.]] Автоматный алгоритм model checking для LTL: общая схема.
  
−
'''[[Media: Seminar_Verification_7_spin_manual.pdf| Инструкция по работе со средством SPIN.]]'''
+
[[Media: Verif_VP_15.pdf|Блок 15.]] Автоматы Бюхи. Обобщённые автоматы Бюхи.
  
−
'''[[Media: Seminar_Verification_8.pdf| Семинар 8-9.]]''' SPIN: практические задания по проверке LTL-спецификаций.
+
[[Media: Verif_VP_16.pdf|Блок 16.]] Пересечение автоматов Бюхи.
  
−
'''[[Media: Seminar_Verification_10.pdf| Семинар 10.]]''' UPPAAL: практические задания по проверке временных спецификаций.
+
[[Media: Verif_VP_17.pdf|Блок 17.]] Проверка пустоты автомата Бюхи.
  
−
'''[[Media: Seminar_Verification_10_errors.zip| Архив, прилагающийся к семинару 10.]]
+
[[Media: Verif_VP_18.pdf|Блок 18.]] Автоматы Бюхи для моделей Крипке
  
−
= Правила проведения экзамена =
+
[[Media: Verif_VP_19.pdf|Блок 19.]] Автоматы Бюхи для ltl-формул.
  
−
<ol>
+
[[Media: Verif_VP_20.pdf|Блок 20.]] Автоматный алгоритм model checking для LTL: уточнённая схема.
−
<li> Экзамен по курсу "Математические методы верификации схем и программ " состоится 14 января в ауд. П-14; начало экзамена - 10.00; окончание экзамена - 12.00.
+
−
<li> Итоговая экзаменационная оценка складывается из оценки за экзаменационную контрольную работу, зачетных оценок за выполнение домашних заданий и премиальных оценок за решение особо сложных задач, объявленных в курсе лекций.
+
−
<li> Экзаменационная контрольная работа состоит из 5 задач и 5 вопросов. Каждая из задач контрольной относится к одному из типов задач, которые разбирались на семинарских занятиях или на лекциях. Каждый из вопросов касается формулировок определений или ключевых результатов, рассмотренных на лекциях.
+
−
<li> Выставление экзаменационных оценок и ознакомление с работами будет проводиться 14 января в ауд. 506 в 17.00.
+
−
<li> Консультация к экзамену состоится 12 января в ауд. 506 в 16.30.
+
−
</ol>
+
  
−
== Учет домашних заданий ==
+
[[Media: Verif_VP_21.pdf|Блок 21.]] Логика деревьев вычислений (CTL). Постановка задачи верификации моделей Крипке относительно CTL.
  
−
'''Домашнее задание 1:''' предоставившие решение этого задания освобождаются от решения задачи на тему логики Хоара.
+
[[Media: Verif_VP_22.pdf|Блок 22.]] Базовый алгоритм model checking для CTL.
  
−
'''Домашние задания 3, 4:''' предоставившие решения этих заданий будут освобождены от задач, покрываемых темами заданий, а также (задание 4) поощрены дополнительными баллами на экзамене.
+
[[Media: Verif_VP_23.pdf|Блок 23.]] Справедливость и CTL.
  
−
'''Домашние задания 5, 6, 7 (NuSMV, Spin, Uppaal):'''
+
[[Media: Verif_VP_24.pdf|Блок 24.]] Символьные представления моделей.
−
* если решены ровно два из трёх заданий, то из итоговой оценки (''2'', ''3'', ''4'', ''5'') вычитается один балл;
+
−
* если решено менее двух заданий, то из итоговой оценки вычитается два балла.
+
  
−
'''По окончании семестра снова открывается прием заявок на получение домашних заданий 5, 6, 7.''' Правила получения домашних заданий - в разделе домашних заданий. Крайний срок сдачи: '''сутки до экзамена'''. Решения, сданные позднее крайнего срока, могут быть не учтены на экзамене. '''Внимание:''' неправильно работающие решения, сданные вблизи крайнего срока, могут быть не приняты ввиду задержек, требуемых для их проверки, отправки на доработку, доработки и повторной проверки.
+
[[Media: Verif_VP_25.pdf|Блок 25.]] Двоичные решающие диаграммы: BDD, OBDD, ROBDD.
  
−
= Домашние задания =
+
[[Media: Verif_VP_26.pdf|Блок 26.]] Символьный алгоритм model checking для CTL (начало).
  
−
Решение домашних заданий, а также ''любые'' вопросы по домашним заданиям можно высылать на почту [[Подымов Владислав Васильевич| valdus@yandex.ru]].
+
[[Media: Verif_VP_27.pdf|Блок 27.]] Преобразователи предикатов и их неподвижные точки.
  
−
== Домашнее задание 1: логика Хоара ==
+
[[Media: Verif_VP_28.pdf|Блок 28.]] Символьный алгоритм model checking для CTL (окончание).
  
−
Домашнее задание сформулировано в слайдах семинара 1.
+
[[Media: Verif_VP_29.pdf|Блок 29.]] CTL*. CTL и LTL как фрагменты CTL*. Сравнение выразительности CTL и LTL.
  
−
Решение должно быть нерукописным (.txt, .doc, TeX-pdf, ...).
+
[[Media: Verif_VP_30.pdf|Блок 30.]] Системы реального времени (СРВ). Временные автоматы.
  
−
Крайний срок сдачи: '''27 сентября, 23:59'''.
+
[[Media: Verif_VP_31.pdf|Блок 31.]] Неправдоподобные вычисления временных автоматов.
  
−
Поощрение за сделанное домашнее задание: '''освобождение от задачи на тему логики Хоара'''.
+
[[Media: Verif_VP_32.pdf|Блок 32.]] Логика ветвящегося реального времени (TCTL). Задача model checking для TCTL.
  
−
== Домашнее задание 2, обязательное: установка средств верификации ==
+
[[Media: Verif_VP_33.pdf|Блок 33.]] Сети временных автоматов.
  
−
* (''прежде всего'') поставить [http://nusmv.fbk.eu NuSMV]
+
[[Media: Verif_VP_34.pdf|Блок 34.]] Алгоритм model checking для TCTL. Временные регионы. Системы регионов.
−
* (''чуть позже, но тоже надо'') поставить [http://spinroot.com Spin]
+
−
* (''ещё позже, но тоже надо'') поставить [http://uppaal.org UPPAAL] (''лучше версию 4.0, но можно и последнюю'')
+
−
* настоятельно рекомендуется всё это поставить в Linux (''с Windows у студентов постоянно возникают странные проблемы, а в Linux всё работает - проверено'')
+
−
* проверить, что всё это работает:
+
−
** в выводе "'''./NuSMV'''" есть строки, утверждающие, что
+
−
*** подключены CUDD и MiniSat, либо нет строк о том, что что-то надо подключить
+
−
*** входной файл не подан и работа завершена
+
−
** "'''./spin -a <папка с примерами spin>/LTL/bakery.pml'''" успешно завершает работу без вывода
+
−
** "'''./uppaal'''" загружает графический интерфейс и для какого-нибудь примера при нажатии на кнопку '''Check''' вкладки '''Verifier''' при каком-нибудь выделенном свойстве завершает вывод словами '''Property is satisfied''' или '''Property is not satisfied'''
+
−
* '''Организовать хотя бы один ноутбук на двоих (если совсем не выходит, то на троих) с поставленным NuSMV на занятии 21.10.2016'''
+
  
−
== Домашнее задание 3: формализация систем и свойств, алгоритмы проверки CTL-формул ==
+
[[Media: Verif_VP_35.pdf|Блок 35.]] Отношения симуляции и бисимуляции. Симуляционная и бисимуляционная эквивалентности.
  
−
* написать письмо с любым содержанием и заголовком "'''[Ver 2016 hw2] Фамилия И.О.'''"
+
[[Media: Verif_VP_36.pdf|Блок 36.]] Бисимуляция состояний модели. Алгоритм проверки бисимуляционной эквивалентности. Фактор-модель.
−
* в ответ будут присланы описание системы и требований к этой системе
+
−
* задача: поработать в качестве табличного или символьного алгоритма верификации CTL-формул и донести результат в любом виде
+
−
** табличный алгоритм:
+
−
*** нарисовать модель Крипке
+
−
*** записать требования в виде CTL-формул
+
−
*** описать шаги работы алгоритма настолько (''не'')строго, чтобы можно было без чрезмерных усилий строго восстановить каждый шаг работы
+
−
** символьный алгоритм:
+
−
*** записать набор формул для модели Крипке
+
−
*** записать требования в виде CTL-формул
+
−
*** описать шаги работы алгоритма (включающие BDD, QBF или аналогичную формальную запись) настолько (''не'')строго, чтобы можно было без чрезмерных усилий строго восстановить каждый шаг работы
+
  
−
== Домашнее задание 4, сложное: символьный алгоритм проверки CTL-формул ==
+
[[Media: Verif_VP_37.pdf|Блок 37.]] Абстракция моделей. Редукция по конусу влияния. Абстракция данных.
  
−
* этим заданием покрывается домашнее задание 3
+
[[Media: Verif_VP_38.pdf|Блок 38.]] Bounded model checking (BMC), постановка.
−
* привести описание символьного алгоритма верификации CTL-формул, работающего в условиях справедливости для CTL
+
−
** можно написать псевдокод с пояснениями
+
−
** можно описать на естественном языке, но так, чтобы можно было без чрезмерных усилий строго восстановить каждый шаг работы алгоритма
+
−
** можно написать программу
+
−
** ...
+
−
* привести пример работы алгоритма, иллюстрирующий его отличие от "несправедливого" символьного алгоритма
+
  
−
== Домашнее задание 5, обязательное: NuSMV ==
+
[[Media: Verif_VP_39.pdf|Блок 39.]] Проблема выполнимости булевых формул (SAT).
  
−
'''Внимание,''' в связи с неоднократными просьбами и неожиданным осознанием сдающих, что в NuSMV всё не так просто, крайний срок домашнего задания сдвинут на несколько дней: '''20.11.2016, 23:59'''.
+
[[Media: Verif_VP_40.pdf|Блок 40.]] Решение BMC с помощью SAT.
  
−
* задание можно выполнять как в одиночку, так и в паре
+
''Материалы будут появляться по мере проведения занятий.''
−
* написать письмо с любым содержанием и заголовком
+
−
** "'''[Ver 2016 nusmv] Фамилия И.О.'''", если задание выполняется в одиночку
+
−
** "'''[Ver 2016 nusmv] Фамилия И.О. Фамилия И.О.'''", если задание выполняется в паре
+
−
* в ответ будут присланы описание системы и требований к ней
+
−
* задача: описать систему и требования в формате NuSMV так, чтобы можно было проверить требования обычным для NuSMV образом
+
−
* необходимо выслать ответом на присланное письмо файл с расширением .smv, содержащий описание системы и требований в формате NuSMV
+
−
* если есть предпочтения: из какой области хотелось бы видеть описание системы - то эти предпочтения можно выразить в тексте первого письма
+
−
** если предпочтения разумны, то они могут быть учтены
+
−
** например, на семинаре 5 было озвучено несколько таких областей: параллельно работающие программы, схемы, игры/головоломки, системы общего вида
+
−
* крайний срок сдачи: '''20.11.2016, 23:59'''
+
−
* поощрение за выполненное домашнее задание: '''необходимо для допуска к экзамену'''
+
−
* наказание за невыполненное домашнее задание: '''сдача этого задания перед экзаменом в более сжатые сроки'''
+
−
* в зависимости от степени ошибочности решение может быть принято, не принято или отправлено на доработку; последнее - в том случае, если в системе есть существенные недостатки, но в достаточном количестве присутствуют правильно реализованные разумные идеи
+
−
** рекомендуется задействовать все средства, позволяющие убедиться, что система и требования описаны правильно
+
−
** если задание выполняется в паре, рекомендуется каждому участнику проверить правильность итогового .smv-файла
+
  
−
== Домашнее задание 6, обязательное: Spin ==
+
== Прошлогодние ==
  
−
* задание можно выполнять как в одиночку, так и в паре
+
[[Media: Verif_VP_all.pdf|Все слайды лекций в одном файле.]]
−
* написать письмо с любым содержанием и заголовком
+
−
** "'''[Ver 2016 spin] Фамилия И.О.'''", если задание выполняется в одиночку
+
−
** "'''[Ver 2016 spin] Фамилия И.О. Фамилия И.О.'''", если задание выполняется в паре
+
−
* в ответ будут присланы описание системы и требований к ней
+
−
* задача: описать систему и требования на языке PROMELA так, чтобы можно было проверить требования обычным для средства SPIN образом
+
−
* необходимо выслать ответом на присланное письмо файл с расширением .pml, содержащий описание системы и требований на языке PROMELA
+
−
* если есть предпочтения: из какой области хотелось бы видеть описание системы - то эти предпочтения можно выразить в тексте первого письма
+
−
* крайний срок сдачи: '''06.12.2016, 23:59'''
+
−
* поощрение за выполненное домашнее задание: '''необходимо для допуска к экзамену'''
+
−
* наказание за невыполненное домашнее задание: '''сдача этого задания перед экзаменом в более сжатые сроки'''
+
−
* в зависимости от степени ошибочности решение может быть принято, не принято или отправлено на доработку; последнее - в том случае, если в системе есть существенные недостатки, но в достаточном количестве присутствуют правильно реализованные разумные идеи
+
−
** рекомендуется задействовать все средства, позволяющие убедиться, что система и требования описаны правильно
+
−
** если задание выполняется в паре, рекомендуется каждому участнику проверить правильность итогового .pml-файла
+
  
−
== Домашнее задание 7, обязательное: Uppaal ==
+
= Семинары =
  
−
* задание можно выполнять как в одиночку, так и в паре
+
[[Media: Verif_VP_sem01.pdf|Семинар 1.]] Дедуктивная верификация императивных программ.
−
* написать письмо с любым содержанием и заголовком
+
 
−
** "'''[Ver 2016 uppaal] Фамилия И.О.'''", если задание выполняется в одиночку
+
[[Media: Verif_VP_sem02.pdf|Семинар 2.]] Модели Крипке. LTL. Безопасность и живость. Справедливость.
−
** "'''[Ver 2016 uppaal] Фамилия И.О. Фамилия И.О.'''", если задание выполняется в паре
+
 
−
* в ответ будут присланы описание системы и задачу, которую требуется решить для этой системы
+
[[Media: Verif_VP_sem03.pdf|Семинар 3.]] CTL. Базовый алгоритм model checking для CTL. BDD.
−
* задача: описать систему в GUI Uppaal, а также составить в этом же GUI набор формул, по результатам проверки которых можно легко выяснить ответ к задаче
+
 
−
* необходимо выслать ответом на присланное письмо два файла, генерируемые GUI Uppaal: с расширением .xml (описание системы) и с расширением .q (описание требований)
+
''Материалы будут появляться по мере проведения занятий.''
−
* если есть предпочтения, относящиеся к виду анализируемой системы, можно их выражать в тексте первого письма
+
 
−
* крайний срок сдачи: '''20.12.2016, 23:59'''
+
= Обязательные домашние задания =
−
* поощрение за выполненное домашнее задание: '''необходимо для допуска к экзамену'''
+
 
−
* наказание за невыполненное домашнее задание: '''сдача этого задания перед экзаменом в более сжатые сроки'''
+
Курсом предполагаются три обязательных домашних задания: "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:
 +
** можно написать псевдокод с пояснениями,
 +
** можно описать на естественном языке, но так, чтобы можно было без чрезмерных усилий строго восстановить каждый шаг работы алгоритма,
 +
** можно написать программу,
 +
** ...;
 +
* привести пример работы алгоритма, иллюстрирующий его отличие от "несправедливого" символьного алгоритма.
  
 
= Литература =
 
= Литература =
Строка 186: Строка 251:
 
#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.
−
 
+
−
[[Категория:Лекционные курсы кафедры МК]]
+
−
[[Категория:Магистерская программа Дискретные управляющие системы и их приложения]]
+

Текущая версия на 10:34, 20 ноября 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=11562»