Город: Санкт-Петербург Новосибирск Казань Язык: Русский English

Введение в моделирование и верификацию аппаратных и программных систем
Санкт-Петербург / осень 2007, посмотреть все семестры

Запишитесь на курс, чтобы получать уведомления и иметь возможность сдавать домашние задания. Для записи требуется регистрация на сайте.
Перейти к регистрации Войти

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

  • реактивные системы и их моделирование;
  • временные логики;
  • метод проверки моделей (model checking) и алгоритмы для проверки моделей;
  • задача булевой выполнимости и ее роль в верификации аппаратных и программных систем.

Наряду с теоретическими основами верификации будут рассмотрены программные средства для верификации и примеры.

Дата и время Занятие Место Материалы
20 октября
17:00–18:30
Введение, Лекция ПОМИ РАН слайды
20 октября
18:40–20:10
Системы переходов для моделирования систем, Лекция ПОМИ РАН слайды
21 октября
17:15–18:45
Логика линейного времени, Лекция ПОМИ РАН слайды
21 октября
19:00–20:30
Дедуктивная LTL верификация, Лекция ПОМИ РАН слайды
21 октября
19:00–20:30
Логика деревьев вычислений CTL, Лекция ПОМИ РАН слайды
21 октября
20:30–22:00
Проверка моделей на практике, Лекция ПОМИ РАН слайды
21 октября
20:30–22:00
Двоичные разрешающие диаграммы (BDD). Символьная проверка моделей, Лекция ПОМИ РАН слайды
03 ноября
17:25–18:55
Представление с неподвижной точкой. Условия справедливости. Синтез OBDD, Лекция ПОМИ РАН слайды
03 ноября
17:25–18:55
Разделенная нормальная форма для логики линейного времени LTL: определение и приведение к разделенной нормальной форме с условными обязательствами, Лекция ПОМИ РАН слайды
04 ноября
17:30–19:00
Разделенная нормальная форма для логики линейного времени LTL: условные обязательства и построение автомата, Лекция ПОМИ РАН слайды
04 ноября
17:30–19:00
Автоматный подход, Лекция ПОМИ РАН слайды
04 ноября
17:30–19:00
Проверка моделей ограниченной глубины, Лекция ПОМИ РАН слайды
04 ноября
19:15–20:45
Свидетельства и контрпримеры. Абстракция, Лекция ПОМИ РАН слайды
04 ноября
19:15–20:45
Заключение и чего же ожидать в экзамене, Лекция ПОМИ РАН слайды