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

Материал из Кафедра математической кибернетики
Перейти к: навигация, поиск
м
(не показаны 47 промежуточные версии 2 участников)
Строка 2: Строка 2:
  
  
Обязательный курс для магистров 618/2 и 621 групп 3 семестра магистратуры.  
+
Обязательный курс для магистров групп 618мк_дс, 618мк_дус и 621асвк 3 семестра магистратуры (группа 621асвк - "Методы верификации программ").  
  
Курс читают  
+
В 2021/2022 учебном году курс читают  
  
* профессор [[Захаров Владимир Анатольевич|В. А. Захаров]]
+
* [[Захаров Владимир Анатольевич|В. А. Захаров]]
* младший научный сотрудник [[Подымов Владислав Васильевич|В. В. Подымов]].
+
* [[Подымов Владислав Васильевич|В. В. Подымов]].
  
Лекционная нагрузка — 32 ч., семинары и практические занятия— 16 ч.
+
<!-- Лекционная нагрузка — 32 ч., семинары и практические занятия— 16 ч. -->
  
 
= Программа =
 
= Программа =
 +
 +
Видеозаписи лекций размещены по адресу [https://m.cs.msu.ru/index.php/s/N6FkcmFbxQkS8z9] в разделе '''ЗахаровВА'''
  
 
''Программа будет обновляться по мере проведения занятий.''
 
''Программа будет обновляться по мере проведения занятий.''
  
#Задача верификации аппаратуры и программного обеспечения. Зачем нужна формальная верификация программ? Основные подходы к задаче формальной верификации. Принципы верификации моделей программ. Исторические сведения. Достижения методов формальной верификации программ. Алгоритмические и комбинаторные трудности применения метода верификации моделей программ. '''[[Media: Lecture_Verification_1.pdf| Лекция 1.]]'''
+
#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_2.pdf| Лекция 2.]]'''
+
<!-- '''[[Media: Lecture_Verification_1.pdf| Лекция 1.]]''' -->
#Моделирование схем. Системы переходов - модели Крипке. Представление систем переходов формулами логики предикатов первого порядка. Синхронные и асинхронные схемы. Степень детализации представления. Трансляция описаний программ и схем в модели Крипке. '''[[Media: Lecture_Verification_3.pdf| Лекция 3.]]'''
+
#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.]]'''
#Темпоральная логика деревьев вычислений CTL. Синтаксис и семантика CTL. Примеры спецификаций моделей в терминах формул CTL. Темпоральная логика линейного времени PLTL. Синтаксис и семантика PLTL. Свойства живости и безопасности. Ограничения справедливости. Задача верификации моделей (model-checking). '''[[Media: Lecture_Verification_4.pdf| Лекция 4.]]'''
+
<!-- '''[[Media: Lecture_Verification_2.pdf| Лекция 2.]]''' -->
#Табличный алгоритм верификации моделей для CTL. Обоснование корректности и сложности табличного алгоритма верификации моделей. Проблема “комбинаторного взрыва”. Символьные средства описания моделей. Двоичные разрешающие диаграммы (BDD). Алгоритм редукции BDD к каноническому виду (OBDD). Выполнение операций над OBDD: унарные и бинарные булевы операции, квантификация, проверка выполнимости, подсчет числа единиц. Общие представления о сложности в классе OBDD. '''[[Media: Lecture_Verification_5.pdf| Лекция 5.]]'''
+
#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.]]'''
#Представления неподвижной точки в CTL. Алгоритм символьной верификации моделей в CTL. '''[[Media: Lecture_Verification_6.pdf| Лекция 6.]]'''
+
#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.]]'''
#Табличная верификация моделей для PLTL. Автоматы Бюхи: их свойства и обобщения. Трансляция формул PLTL в автоматы Бюхи. Сведение задачи проверки выполнимости формул PLTL к проблеме пустоты для автоматов Бюхи. <!-- Алгоритм двойного поиска в глубину с возвратом (DDFS) для проверки пустоты автоматов Бюхи. --> '''[[Media: Lecture_Verification_7.pdf| Лекция 7.]]'''
+
#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.]]'''
<!-- #Особенности параллельных вычислений асинхронных распределенных систем. Независимость действий. Проскальзывающие действия. Достаточные множества переходов и их свойства. Вычисление достаточных множеств переходов. Статическая и динамическая редукция частичных порядков на основе достаточных множеств переходов. '''[[Media: Lecture_Verification_8.pdf| Лекция 8.]]''' -->
+
#Basics of Fixed Point Theory. Fixed point characterization of CTL temporal operators. Symbolic model checking algorithm for CTL. '''[[Media: Lecture_Verification_6.pdf| Лекция 6.]]'''
#Отношения бисимуляционной эквивалентности (бисимуляции) и симуляционного квазипорядка (симуляции) на моделях Крипке. Равновыполнимость темпоральных формул на бисимуляционно эквивалентных моделях Крипке. Вычисление классов бисимуляционной эквивалентности на конечных моделях Крипке. Упрощение моделей Крипке при помощи отношений симуляции и и бисимуляции. Редукция моделей Крипке по конусу влияния. Абстракции данных при построении моделей Крипке. '''[[Media: Lecture_Verification_8.pdf| Лекция 8.]]'''
+
#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.]]'''
#Временные автоматы как формальные модели распределенных систем реального времени. Вычисления временных автоматов. Примеры использования временных автоматов для моделирования встроенных систем. Зеноновские вычисления. Синтаксис и семантика Timed CTL. Примеры формальных спецификаций поведения встроенных систем при помощи TCTL. '''[[Media: Lecture_Verification_9.pdf| Лекция 9.]]'''
+
<!-- #Особенности параллельных вычислений асинхронных распределенных систем. Независимость действий. Проскальзывающие действия. Достаточные множества переходов и их свойства. Вычисление достаточных множеств переходов. Статическая и динамическая редукция частичных порядков на основе достаточных множеств переходов. <!--'''[[Media: Lecture_Verification_8.pdf| Лекция 8.]]''' -->
#Задача верификации моделей программ реального времени. Отношение эквивалентности часов и регионы. Регионные системы переходов. Оценка числа регионов. Сведение задачи верификации временных автоматов относительно TCTL к задаче верификации моделей Крипке относительно CTL. '''[[Media: Lecture_Verification_10.pdf| Лекция 10.]]'''
+
# 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.]]'''
#Верификация моделей программ для вычислений ограниченной длины (bounded model checking, BMC). Сведение задачи BMC к задаче проверки выполнимости булевых формул (SAT). Применение автоматических средств решения задачи SAT для решения задачи BMC. '''[[Media: Lecture_Verification_11.pdf| Лекция 11.]]'''
+
#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.]]'''
  
 
= Материалы семинаров =
 
= Материалы семинаров =
Строка 32: Строка 36:
 
''Материалы будут обновляться по мере проведения занятий.''
 
''Материалы будут обновляться по мере проведения занятий.''
  
''Любые'' вопросы по темам семинарских занятий можно высылать на почту [[Подымов Владислав Васильевич| valdus@yandex.ru]].
+
'''Любые''' вопросы по темам семинарских занятий можно задавать [[Подымов Владислав Васильевич|ему]].
  
'''[[Media: Seminar_Verification_1.pdf| Семинар 1.]]''' Доказательство корректности императивных программ с помощью логики Хоара.
+
'''[[Media: Seminar_Verification_1_eng.pdf| Seminar 1.]]''' Deductive verification of imperative programs based on Hoare logic.
  
'''[[Media: Seminar_Verification_2.pdf| Семинар 2.]]''' Модели Крипке. LTL, CTL. Безопасность, живость, справедливость.
+
'''[[Media: Seminar_Verification_2_eng.pdf| Seminar 2.]]''' Kripke structures. LTL. Safety and liveness. Fairness.
  
'''[[Media: Seminar_Verification_3.pdf| Семинар 3.]]''' Табличный и символьный алгоритмы проверки CTL-формул на моделях Крипке. ROBDD.
+
'''[[Media: Seminar_Verification_3_eng.pdf| Seminar 3.]]''' CTL. BDD. Model checking for CTL: tableaux-based algorithm, symbolic algorithm.
  
'''[[Media: Seminar_Verification_4.pdf| Семинар 4.]]''' Обзор средства NuSMV: описание параллельной композиции автоматов, проверка CTL-формул.
+
'''[[Media: Seminar_Verification_4_eng.pdf| Seminar 4.]]''' NuSMV tool overview.
  
'''[[Media: Seminar_Verification_5.pdf| Семинар 5-6.]]''' NuSMV: практические задания по проверке CTL-спецификаций.
+
'''[[Media: Seminar_Verification_5_eng.pdf| Seminar 5-6.]]''' NuSMV exercises.
  
'''[[Media: Seminar_Verification_7.pdf| Семинар 7.]]''' Обзор средства SPIN: синтаксис, трансляция базовых конструкций в модели Крипке.
+
'''[[Media: Seminar_Verification_7_eng.pdf| Seminar 7.]]''' Spin tool overview.
  
'''[[Media: Seminar_Verification_7_spin_manual.pdf| Инструкция по работе со средством SPIN.]]'''
+
'''[[Media: Seminar_Verification_7_spin_manual.pdf| (Deprecated) Some Spin instruction (rus).]]'''
  
'''[[Media: Seminar_Verification_8.pdf| Семинар 8-9.]]''' SPIN: практические задания по проверке LTL-спецификаций.
+
'''[[Media: Seminar_Verification_8_eng.pdf| Seminar 8-9.]]''' SPIN exercises.
  
'''[[Media: Seminar_Verification_10.pdf| Семинар 10.]]''' UPPAAL: практические задания по проверке временных спецификаций.
+
'''[[Media: Seminar_Verification_10_eng.pdf| Seminar 10-11.]]''' UPPAAL exercises.
  
'''[[Media: Seminar_Verification_10_errors.zip| Архив, прилагающийся к семинару 10.]]
+
'''[[Media: Seminar_Verification_10_errors.zip| Zip-file required for the last exercises of Seminar 10-11.]]
  
 
= Правила проведения экзамена =
 
= Правила проведения экзамена =
  
<ol>
+
# Итоговая экзаменационная оценка складывается из оценки за экзаменационную контрольную работу, зачетных оценок за выполнение домашних заданий и премиальных оценок за решение особо сложных задач, объявленных в курсе лекций.
<li> Экзамен по курсу "Математические методы верификации схем и программ " состоится 14 января в ауд. П-14; начало экзамена - 10.00; окончание экзамена - 12.00.
+
# Экзаменационная контрольная работа состоит из 5 задач и 5 вопросов. Каждая из задач контрольной относится к одному из типов задач, которые разбирались на семинарских занятиях или на лекциях. Каждый из вопросов касается формулировок определений или ключевых результатов, рассмотренных на лекциях.
<li> Итоговая экзаменационная оценка складывается из оценки за экзаменационную контрольную работу, зачетных оценок за выполнение домашних заданий и премиальных оценок за решение особо сложных задач, объявленных в курсе лекций.
+
<li> Экзаменационная контрольная работа состоит из 5 задач и 5 вопросов. Каждая из задач контрольной относится к одному из типов задач, которые разбирались на семинарских занятиях или на лекциях. Каждый из вопросов касается формулировок определений или ключевых результатов, рассмотренных на лекциях.
+
<li> Выставление экзаменационных оценок и ознакомление с работами будет проводиться 14 января в ауд. 506 в 17.00.
+
<li> Консультация к экзамену состоится 12 января в ауд. 506 в 16.30.
+
</ol>
+
  
 
== Учет домашних заданий ==
 
== Учет домашних заданий ==
  
'''Домашнее задание 1:''' предоставившие решение этого задания освобождаются от решения задачи на тему логики Хоара.
+
'''Логика Хоара:''' выполнившие это задание освобождаются от решения задачи на тему логики Хоара, и за особые заслуги могут быть поощрены дополнительной премиальной оценкой.
  
'''Домашние задания 3, 4:''' предоставившие решения этих заданий будут освобождены от задач, покрываемых темами заданий, а также (задание 4) поощрены дополнительными баллами на экзамене.
+
'''CTL: формализация требований и алгоритмы проверки формул:''' выполнившие это задание освобождаются от задач, покрываемых темами заданий, и могут быть поощрены дополнительной премиальной оценкой за особые заслуги (например, демонстрацию хорошего понимания устройства символьного алгоритма).
  
'''Домашние задания 5, 6, 7 (NuSMV, Spin, Uppaal):'''
+
'''CTL и справедливость:''' этим заданием покрывается часть задания "алгоритм верификации CTL-формул", и кроме того, выполнившие это задание будут поощрены дополнительной премиальной оценкой.
* если решены ровно два из трёх заданий, то из итоговой оценки (''2'', ''3'', ''4'', ''5'') вычитается один балл;
+
* если решено менее двух заданий, то из итоговой оценки вычитается два балла.
+
  
'''По окончании семестра снова открывается прием заявок на получение домашних заданий 5, 6, 7.''' Правила получения домашних заданий - в разделе домашних заданий. Крайний срок сдачи: '''сутки до экзамена'''. Решения, сданные позднее крайнего срока, могут быть не учтены на экзамене. '''Внимание:''' неправильно работающие решения, сданные вблизи крайнего срока, могут быть не приняты ввиду задержек, требуемых для их проверки, отправки на доработку, доработки и повторной проверки.
+
'''NuSMV, Spin, Uppaal:'''
 +
* если выполнены ровно два из трёх заданий, то из итоговой экзаменационной оценки (''2'', ''3'', ''4'', ''5'') вычитается один балл;
 +
* если выполнено менее двух заданий, то из итоговой экзаменационной оценки вычитается два балла.
  
= Домашние задания =
+
= Обязательные домашние задания "NuSMV", "Spin", "Uppaal" =
  
Решение домашних заданий, а также ''любые'' вопросы по домашним заданиям можно высылать на почту [[Подымов Владислав Васильевич| valdus@yandex.ru]].
+
Решение домашних заданий, а также ''любые'' вопросы по домашним заданиям можно высылать на почту [[Подымов Владислав Васильевич|ему]].
  
== Домашнее задание 1: логика Хоара ==
+
== Установка средств верификации ==
  
Домашнее задание сформулировано в слайдах семинара 1.
+
* Для выполнения обязательных домашних заданий необходимо поставить на свою рабочую машину средства [http://nusmv.fbk.eu NuSMV], [http://spinroot.com Spin] и [http://uppaal.org 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'''.
 +
* '''Для работы на семинарах, посвящённых средствам верификации, требуется организовать хотя бы один ноутбук на двоих (если совсем не выходит, то на троих) с установленными соответствующими средствами верификации.'''
  
Решение должно быть нерукописным (.txt, .doc, TeX-pdf, ...).
+
== Общие правила выполнения заданий "NuSMV", "Spin" и "Uppaal" ==
  
Крайний срок сдачи: '''27 сентября, 23:59'''.
+
* Каждое из заданий можно выполнять как в одиночку, так и в паре.
 +
* Срок выполнения задания (кроме индивидуально согласованных случаев) - от начала проведения соответствующих семинаров и до начала проведения следующего тематического блока семинаров (для последнего блока семинаров - до окончания семестра).
 +
* Первый шаг выполнения - выслать [[Подымов Владислав Васильевич|ему]] на почту письмо с любым текстом и специальным заголовком:
 +
** для выполнения задания "NuSMV" в одиночку: '''[ver-nusmv] группа Фамилия И.О.'''
 +
** для выполнения задания "NuSMV" в паре: '''[ver-nusmv] группа Фамилия И.О., Фамилия И.О.'''
 +
** для выполнения задания "Spin" в одиночку: '''[ver-spin] группа Фамилия И.О.'''
 +
** для выполнения задания "Spin" в паре: '''[ver-spin] группа Фамилия И.О., Фамилия И.О.'''
 +
** для выполнения задания "Uppaal" в одиночку: '''[ver-uppaal] группа Фамилия И.О.'''
 +
** для выполнения задания "Uppaal" в паре: '''[ver-uppaal] группа Фамилия И.О., Фамилия И.О.'''
 +
* В ответ будет выслано письмо, содержащее описание системы и цели исследования этой системы при помощи проверки требований.
 +
* В тексте первого письма можно сформулировать пожелания по виду системы и целей исследования, вплоть до полной формулировки:
 +
** если пожелания разумны, они с немалой вероятностью будут учтены в задании;
 +
** типовые примеры пожеланий: "хочу исследовать параллельно работающие программы", "... схему", "... игру/головоломку", "... систему общего вида, без программистско-математической специализации".
 +
* Решение задания должно быть выслано в ответ на письмо с формулировкой задания в установленный срок.
 +
* Присланное решение
 +
** принимается, если оно полностью или с незначительными недочётами верно;
 +
** не принимается, если оно демонстрирует, что выполнявшие его не пытались вдумчиво разобраться в принципах работы со средством верификации;
 +
** отправляется на доработку, если оно содержит существенные ошибки, но демонстрирует осознанную и правильную работу со средством верификации.
  
Поощрение за сделанное домашнее задание: '''освобождение от задачи на тему логики Хоара'''.
+
== NuSMV ==
  
== Домашнее задание 2, обязательное: установка средств верификации ==
+
Решение этого задания - это
 +
* файл с расширением ".smv", содержащий формализацию системы и требований в формате средства NuSMV, и
 +
* пояснение того, как результаты проверки требований, выдаваемые NuSMV, соотносятся с поставленными целями, в свободной форме.
  
* (''прежде всего'') поставить [http://nusmv.fbk.eu NuSMV]
+
== Spin ==
* (''чуть позже, но тоже надо'') поставить [http://spinroot.com Spin]
+
 
* (''ещё позже, но тоже надо'') поставить [http://uppaal.org UPPAAL] (''лучше версию 4.0, но можно и последнюю'')
+
Решение этого задания - это
* настоятельно рекомендуется всё это поставить в Linux (''с Windows у студентов постоянно возникают странные проблемы, а в Linux всё работает - проверено'')
+
* файл с расширением ".pml", содержащий формализацию системы и требований на языке PROMELA, и
* проверить, что всё это работает:
+
* пояснение того, как результаты проверки требований, выдаваемые средством Spin, соотносятся с поставленными целями, в свободной форме.
** в выводе "'''./NuSMV'''" есть строки, утверждающие, что
+
 
*** подключены CUDD и MiniSat, либо нет строк о том, что что-то надо подключить
+
== Uppaal ==
*** входной файл не подан и работа завершена
+
 
** "'''./spin -a <папка с примерами spin>/LTL/bakery.pml'''" успешно завершает работу без вывода
+
Решение этого задания - это
** "'''./uppaal'''" загружает графический интерфейс и для какого-нибудь примера при нажатии на кнопку '''Check''' вкладки '''Verifier''' при каком-нибудь выделенном свойстве завершает вывод словами '''Property is satisfied''' или '''Property is not satisfied'''
+
* файл или файлы, сгенерированные средством Uppaal и содержащие формализацию системы и требований (Uppaal 4.1: файл ".xml"; Uppaal 4.0: файлы ".xml" и ".q"), и
* '''Организовать хотя бы один ноутбук на двоих (если совсем не выходит, то на троих) с поставленным NuSMV на занятии 21.10.2016'''
+
* пояснение того, как результаты проверки требований, выдаваемые средством Uppaal, соотносятся с поставленными целями, в свободной форме.
 +
 
 +
= Поощряемые домашние задания =
 +
 
 +
Решение домашних заданий, а также ''любые'' вопросы по домашним заданиям можно высылать на почту [[Подымов Владислав Васильевич|ему]].
 +
 
 +
== Логика Хоара ==
  
== Домашнее задание 3: формализация систем и свойств, алгоритмы проверки CTL-формул ==
+
Крайний срок выполнения задания: начало семинара 3 (по CTL).
  
* написать письмо с любым содержанием и заголовком "'''[Ver 2016 hw2] Фамилия И.О.'''"
+
Задание сформулировано на последнем слайде материалов семинара 1.
* в ответ будут присланы описание системы и требований к этой системе
+
* задача: поработать в качестве табличного или символьного алгоритма верификации CTL-формул и донести результат в любом виде
+
** табличный алгоритм:
+
*** нарисовать модель Крипке
+
*** записать требования в виде CTL-формул
+
*** описать шаги работы алгоритма настолько (''не'')строго, чтобы можно было без чрезмерных усилий строго восстановить каждый шаг работы
+
** символьный алгоритм:
+
*** записать набор формул для модели Крипке
+
*** записать требования в виде CTL-формул
+
*** описать шаги работы алгоритма (включающие BDD, QBF или аналогичную формальную запись) настолько (''не'')строго, чтобы можно было без чрезмерных усилий строго восстановить каждый шаг работы
+
  
== Домашнее задание 4, сложное: символьный алгоритм проверки CTL-формул ==
+
== CTL: формализация требований и алгоритмы проверки формул ==
  
* этим заданием покрывается домашнее задание 3
+
Крайний срок выполнения задания: конец семестра.
* привести описание символьного алгоритма верификации CTL-формул, работающего в условиях справедливости для CTL
+
** можно написать псевдокод с пояснениями
+
** можно описать на естественном языке, но так, чтобы можно было без чрезмерных усилий строго восстановить каждый шаг работы алгоритма
+
** можно написать программу
+
** ...
+
* привести пример работы алгоритма, иллюстрирующий его отличие от "несправедливого" символьного алгоритма
+
  
== Домашнее задание 5, обязательное: NuSMV ==
+
Как выполнить это задание:
 +
* написать письмо с любым содержанием и заголовком '''[ver-ctl] группа Фамилия И.О.''';
 +
* в ответ будут присланы описание системы и требований к этой системе;
 +
* требуется адекватно формализовать требования в логике ветвящегося времени, изобразить шаги работы табличного или символьного алгоритма и донести результат до [[Подымов Владислав Васильевич|него]] в любом виде.
  
'''Внимание,''' в связи с неоднократными просьбами и неожиданным осознанием сдающих, что в NuSMV всё не так просто, крайний срок домашнего задания сдвинут на несколько дней: '''20.11.2016, 23:59'''.
+
Если сомневаетесь, что означает "изобразить шаги работы алгоритма", то по умолчанию поступайте так:
 +
* табличный алгоритм:
 +
** нарисовать модель Крипке, адекватно описывающую систему;
 +
** описать пошаговое получение разметки алгоритмом настолько (''не'')строго, чтобы можно было без чрезмерных усилий строго восстановить каждый шаг работы алгоритма;
 +
* символьный алгоритм:
 +
** описать модель Крипке в символьной записи (основанной на любом общеизвестном представлении булевых функций);
 +
** описать пошаговое преобразование символьных записей алгоритмом настолько (''не'')строго, чтобы можно было без чрезмерных усилий строго восстановить каждый шаг работы алгоритма.
  
* задание можно выполнять как в одиночку, так и в паре
+
== CTL и справедливость ==
* написать письмо с любым содержанием и заголовком
+
** "'''[Ver 2016 nusmv] Фамилия И.О.'''", если задание выполняется в одиночку
+
** "'''[Ver 2016 nusmv] Фамилия И.О. Фамилия И.О.'''", если задание выполняется в паре
+
* в ответ будут присланы описание системы и требований к ней
+
* задача: описать систему и требования в формате NuSMV так, чтобы можно было проверить требования обычным для NuSMV образом
+
* необходимо выслать ответом на присланное письмо файл с расширением .smv, содержащий описание системы и требований в формате NuSMV
+
* если есть предпочтения: из какой области хотелось бы видеть описание системы - то эти предпочтения можно выразить в тексте первого письма
+
** если предпочтения разумны, то они могут быть учтены
+
** например, на семинаре 5 было озвучено несколько таких областей: параллельно работающие программы, схемы, игры/головоломки, системы общего вида
+
* крайний срок сдачи: '''20.11.2016, 23:59'''
+
* поощрение за выполненное домашнее задание: '''необходимо для допуска к экзамену'''
+
* наказание за невыполненное домашнее задание: '''сдача этого задания перед экзаменом в более сжатые сроки'''
+
* в зависимости от степени ошибочности решение может быть принято, не принято или отправлено на доработку; последнее - в том случае, если в системе есть существенные недостатки, но в достаточном количестве присутствуют правильно реализованные разумные идеи
+
** рекомендуется задействовать все средства, позволяющие убедиться, что система и требования описаны правильно
+
** если задание выполняется в паре, рекомендуется каждому участнику проверить правильность итогового .smv-файла
+
  
== Домашнее задание 6, обязательное: Spin ==
+
Это '''трудное''' домашнее задание.
  
* задание можно выполнять как в одиночку, так и в паре
+
Крайний срок выполнения задания: конец семестра.
* написать письмо с любым содержанием и заголовком
+
** "'''[Ver 2016 spin] Фамилия И.О.'''", если задание выполняется в одиночку
+
** "'''[Ver 2016 spin] Фамилия И.О. Фамилия И.О.'''", если задание выполняется в паре
+
* в ответ будут присланы описание системы и требований к ней
+
* задача: описать систему и требования на языке PROMELA так, чтобы можно было проверить требования обычным для средства SPIN образом
+
* необходимо выслать ответом на присланное письмо файл с расширением .pml, содержащий описание системы и требований на языке PROMELA
+
* если есть предпочтения: из какой области хотелось бы видеть описание системы - то эти предпочтения можно выразить в тексте первого письма
+
* крайний срок сдачи: '''06.12.2016, 23:59'''
+
* поощрение за выполненное домашнее задание: '''необходимо для допуска к экзамену'''
+
* наказание за невыполненное домашнее задание: '''сдача этого задания перед экзаменом в более сжатые сроки'''
+
* в зависимости от степени ошибочности решение может быть принято, не принято или отправлено на доработку; последнее - в том случае, если в системе есть существенные недостатки, но в достаточном количестве присутствуют правильно реализованные разумные идеи
+
** рекомендуется задействовать все средства, позволяющие убедиться, что система и требования описаны правильно
+
** если задание выполняется в паре, рекомендуется каждому участнику проверить правильность итогового .pml-файла
+
  
== Домашнее задание 7, обязательное: Uppaal ==
+
При выполнении этого задания автоматически засчитывается часть задания "CTL: формализация требований и алгоритмы проверки формул", относящаяся к изображению шагов работы алгоритма.
  
* задание можно выполнять как в одиночку, так и в паре
+
Как выполнить это задание:
* написать письмо с любым содержанием и заголовком
+
* предложить описание символьного алгоритма верификации CTL-формул, работающего в условиях справедливости для CTL:
** "'''[Ver 2016 uppaal] Фамилия И.О.'''", если задание выполняется в одиночку
+
** можно написать псевдокод с пояснениями,
** "'''[Ver 2016 uppaal] Фамилия И.О. Фамилия И.О.'''", если задание выполняется в паре
+
** можно описать на естественном языке, но так, чтобы можно было без чрезмерных усилий строго восстановить каждый шаг работы алгоритма,
* в ответ будут присланы описание системы и задачу, которую требуется решить для этой системы
+
** можно написать программу,
* задача: описать систему в GUI Uppaal, а также составить в этом же GUI набор формул, по результатам проверки которых можно легко выяснить ответ к задаче
+
** ...;
* необходимо выслать ответом на присланное письмо два файла, генерируемые GUI Uppaal: с расширением .xml (описание системы) и с расширением .q (описание требований)
+
* привести пример работы алгоритма, иллюстрирующий его отличие от "несправедливого" символьного алгоритма;
* если есть предпочтения, относящиеся к виду анализируемой системы, можно их выражать в тексте первого письма
+
* донести результаты выполнения задания до руководителей курса в любом виде.
* крайний срок сдачи: '''20.12.2016, 23:59'''
+
* поощрение за выполненное домашнее задание: '''необходимо для допуска к экзамену'''
+
* наказание за невыполненное домашнее задание: '''сдача этого задания перед экзаменом в более сжатые сроки'''
+
* в зависимости от степени ошибочности решение может быть принято, не принято или отправлено на доработку; последнее - в том случае, если в системе есть существенные недостатки, но в достаточном количестве присутствуют правильно реализованные разумные идеи
+
  
 
= Литература =
 
= Литература =
Строка 188: Строка 181:
 
#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.
  
  
 
[[Категория:Лекционные курсы кафедры МК]]
 
[[Категория:Лекционные курсы кафедры МК]]
 
[[Категория:Магистерская программа Дискретные управляющие системы и их приложения]]
 
[[Категория:Магистерская программа Дискретные управляющие системы и их приложения]]

Версия 18:48, 27 сентября 2021

Общая информация

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

В 2021/2022 учебном году курс читают


Программа

Видеозаписи лекций размещены по адресу [1] в разделе ЗахаровВА

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

  1. 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. Лекция 1.
  2. 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. Лекция 2.
  3. 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. Лекция 3.
  4. 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. Лекция 4.
  5. 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. Лекция 5.
  6. Basics of Fixed Point Theory. Fixed point characterization of CTL temporal operators. Symbolic model checking algorithm for CTL. Лекция 6.
  7. Model checking problem for LTL. Model checking algorithms for LTL: tableau-based, automata-based. Büchi automata: basic properties and generalizations. Лекция 7.
  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. Лекция 8.
  9. Real-time systems. Timed automata (TA). Infeasible runs of TA. Timed computational tree logic (TCTL). Model checking problem for TCTL. Лекция 9.
  10. A model-checking algorithm for TCTL. Clock and state regions. Region transition systems. Networks of timed automata. Лекция 10.
  11. Bounded model checking (BMC). Reduction of BMC to thr Satisfiability Chercking Problem (SAT). Application of SAT solvers to BMC problem. Лекция 11.

Материалы семинаров

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

Любые вопросы по темам семинарских занятий можно задавать ему.

Seminar 1. Deductive verification of imperative programs based on Hoare logic.

Seminar 2. Kripke structures. LTL. Safety and liveness. Fairness.

Seminar 3. CTL. BDD. Model checking for CTL: tableaux-based algorithm, symbolic algorithm.

Seminar 4. NuSMV tool overview.

Seminar 5-6. NuSMV exercises.

Seminar 7. Spin tool overview.

(Deprecated) Some Spin instruction (rus).

Seminar 8-9. SPIN exercises.

Seminar 10-11. UPPAAL exercises.

Zip-file required for the last exercises of Seminar 10-11.

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

  1. Итоговая экзаменационная оценка складывается из оценки за экзаменационную контрольную работу, зачетных оценок за выполнение домашних заданий и премиальных оценок за решение особо сложных задач, объявленных в курсе лекций.
  2. Экзаменационная контрольная работа состоит из 5 задач и 5 вопросов. Каждая из задач контрольной относится к одному из типов задач, которые разбирались на семинарских занятиях или на лекциях. Каждый из вопросов касается формулировок определений или ключевых результатов, рассмотренных на лекциях.

Учет домашних заданий

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

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

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

NuSMV, Spin, Uppaal:

  • если выполнены ровно два из трёх заданий, то из итоговой экзаменационной оценки (2, 3, 4, 5) вычитается один балл;
  • если выполнено менее двух заданий, то из итоговой экзаменационной оценки вычитается два балла.

Обязательные домашние задания "NuSMV", "Spin", "Uppaal"

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

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

  • Для выполнения обязательных домашних заданий необходимо поставить на свою рабочую машину средства 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, соотносятся с поставленными целями, в свободной форме.

Поощряемые домашние задания

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

Логика Хоара

Крайний срок выполнения задания: начало семинара 3 (по CTL).

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