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

Материал из Кафедра математической кибернетики
Перейти к: навигация, поиск
Строка 11: Строка 11:
 
== Программа ==
 
== Программа ==
  
−
<h4>Часть 1. Математические модели.</h4>
+
#Задача верификации аппаратуры и программного обеспечения. Зачем нужна формальная верификация программ? Основные подходы к задаче формальной верификации. Принципы верификации моделей программ. Исторические сведения. Достижения методов формальной верификации программ. Алгоритмические и комбинаторные трудности применения метода верификации моделей программ. '''[[Media: Lecture_Verification_1.pdf| Лекция 1.]]'''
−
 
+
−
#Характерные особенности и примеры распределенных систем компьютерные сети, локальные и глобальные сети, многопроцессорные компьютеры). Архитектура распределенных систем. Стандарт ISO Open System Interconnection. Алгоритмические проблемы организации вычислений распределенных систем. Особенности распределенных алгоритмов. '''[[Media: DistrAlg_1.pdf| Лекция 1.]]'''
+
−
#Математическая модель распределенных систем. Системы переходов. Синхронный и асинхронный обмен сообщениями. Зависимые и независимые события. Причинно-следственный порядок событий. Эквивалентность выполнений. Вычисления. Логические часы. Топологии распределенных систем. '''[[Media: DistrAlg_2.pdf| Лекция 2.]]'''
+
−
#:
+
−
#:<h4>Часть 2. Коммуникационные протоколы.</h4>
+
−
#:
+
−
#Коммуникационные протоколы. Ошибки, возникающие при передаче сообщений. Задача надежного обмена сообщениями. Симметричные протокол раздвижного окна: устройство протокола и обоснование его корректности. Протокол альтернирующего бита. '''[[Media: DistrAlg_3.pdf| Лекция 3.]]'''
+
−
#Коммуникационный протокол с таймером: устройство и обоснование корректности. '''[[Media: DistrAlg_4.pdf| Лекция 4.]]'''
+
−
#Задача маршрутизации. Алгоритмы построения кратчайших путей в графе. Алгоритм Флойда-Уоршалла. Алгоритм Туэга. Алгоритм Мерлина-Сигала. Алгоритм Чанди-Мизры. '''[[Media: DistrAlg_5.pdf| Лекция 5.]]''' Алгоритм Netchange. '''[[Media: DistrAlg_6.pdf| Лекция 6.]]'''
+
−
#:
+
−
#:<h4>Часть 3. Распределенные алгоритмы.</h4>
+
−
#:
+
−
#Волновые алгоритмы: определение, основные свойства, область применения. Древесный алгоритм. Алгоритм эха. '''[[Media: DistrAlg_7.pdf| Лекция 7.]]''' Фазовый алгоритм. Алгоритм Финна. Алгоритмы обхода. Распределенный обход в глубину. Алгоритмы обхода Авербаха и Сидон. '''[[Media: DistrAlg_8.pdf| Лекция 8.]]'''
+
−
#Задача избрания лидера. Избрание лидера на кольцах: алгоритм Ченя-Робертса, оптимальный алгоритм Патерсона –Долева-Клейва-Роде. '''[[Media: DistrAlg_9.pdf| Лекция 9.]]''' Избрание лидера в произвольных сетях: алгоритм Галладжера-Хамблета-Спиры, алгоритм Кораха-Каттена-Морана. '''[[Media: DistrAlg_10.pdf| Лекция 10.]]'''
+
−
#Задача обнаружения завершения вычисления. Алгоритм Дейкстры-Шолтена. Алгоритм Шави-Франчеза. Алгоритм Сафры. Алгоритм возвращения кредитов. Алгоритм Раны. '''[[Media: DistrAlg_11.pdf| Лекция 11.]]'''
+
−
#Задача сохранения моментального состояния. Алгоритм Чанди-Лампорта. Алгоритм Лаи-Янга. Применение алгоритмов обнаружения моментальной разметки и завершения вычислений для выявления блокировки вычислений. '''[[Media: DistrAlg_12.pdf| Лекция 12.]]'''
+
−
#:
+
−
#:<h4>Часть 4. Вопросы надежности распределенных алгоритмов.</h4>
+
−
#:
+
−
#Задача обеспечения отказоустойчивости распределенных систем. Невозможность построения робастных асинхронных систем. Синхронные робастные алгоритмы принятия решения. Использование криптографических примитивов для повышения отказоустойчивости.
+
−
#Стабилизирующиеся алгоритмы. Пример Дейкстры. Общие принципы построения стабилизирующихся алгоритмов.
+
  
 
== Литература ==
 
== Литература ==
  
−
#G. Tel. Introduction to Distributed Algorithms. Cambridge University Press. 2000. (русск. пер. Ж. Тель. Введение в распределенные алгоритмы, изд-во МЦНМО, 2009 г., 616 с.)
+
#Э.М. Кларк, О. Грамберг, Д. Пелед. Верификация моделей программ: Model Checking. Изд-во МЦНМО, 2002.
 +
#Ю.Г. Карпов. Model Checking: верификация параллельных и распределенных программных систем. Изд-во БХВ-Петербург, 2010.
 +
#K. R. Apt, E.-R. Olderog. Verification of sequential and concurrent programs, Springer, 1997.
 +
#B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, P. Schnoebelen. Systems and Software Verification: Model-Checking Techniques and Tools. Springer, 2001.
 +
#Baier C., Katoen J.-P. Principles of model checking, MIT Press, 2008.  
 +
 
  
 
[[Категория:Лекционные курсы кафедры МК]]
 
[[Категория:Лекционные курсы кафедры МК]]

Версия 13:02, 9 сентября 2016

Обязательный курс для магистров 618 и 621 группы 11 семестра обучения.

Курс читают

профессор В. А. Захаров

младший научный сотрудник В. В. Подымов.

Лекционная нагрузка — 32 ч., семинары и практические занятия— 16 ч.

Программа

  1. Задача верификации аппаратуры и программного обеспечения. Зачем нужна формальная верификация программ? Основные подходы к задаче формальной верификации. Принципы верификации моделей программ. Исторические сведения. Достижения методов формальной верификации программ. Алгоритмические и комбинаторные трудности применения метода верификации моделей программ. Лекция 1.

Литература

  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.
Источник — «https://mk.cs.msu.ru/index.php?title=Математические_методы_верификации_схем_и_программ&oldid=2987»