Введение в моделирование и верификацию аппаратных и программных систем

Общая информация
ЛекторБ. Ю. Конев
Семестросень 2007
Дата начала21.10.2007
Количество пар10
Язык курсарусский
Видеоhttp://www.google.com/search?q=%D0%B1%D0%BE%D1%80%D0%B8%D1%81+%D1%8E%D1%80%D1%8C...
Аннотация Верификация — это проверка того, что аппаратная или программная система соответствует заявленной спецификации (то есть обладает необходимыми свойствами). Данный курс является введением в методы верификации аппаратных и программных систем. В частности, будут освещены следующие темы:
  • реактивные системы и их моделирование;
  • временные логики;
  • метод проверки моделей (model checking) и алгоритмы для проверки моделей;
  • задача булевой выполнимости и ее роль в верификации аппаратных и программных систем.
Наряду с теоретическими основами верификации будут рассмотрены программные средства для верификации и примеры.
Слайды первой лекции
Лекции Подсказка: слайды, видеозапись и другие материалы лекции доступны со страницы лекции, попасть на которую можно, нажав на её название.

1. Введение
(20.10.2007 - 17:00)

http://video.google.com/videoplay?docid=-1300223588197192900
2. Системы переходов для моделирования систем
(20.10.2007 - 17:15)

http://video.google.com/videoplay?docid=-1619785880867648289
3. Логика линейного времени
(21.10.2007 - 17:15)

http://video.google.com/videoplay?docid=6671632546681631328
4. Дедуктивная LTL верификация
(21.10.2007 - 17:20)

http://video.google.com/videoplay?docid=-8844334646541178140
5. Логика деревьев вычислений CTL
(21.10.2007 - 17:25)

http://video.google.com/videoplay?docid=697623268897544006
6. Проверка моделей на практике
(21.10.2007 - 17:30)

http://video.google.com/videoplay?docid=-3297337846295872618
7. Двоичные разрешающие диаграммы (BDD). Символьная проверка моделей
(21.10.2007 - 17:40)

http://video.google.com/videoplay?docid=2999814968611697229
8. Представление с неподвижной точкой. Условия справедливости. Синтез OBDD
(03.11.2007 - 17:25)

http://video.google.com/videoplay?docid=-912528906926339477
9. Разделенная нормальная форма для логики линейного времени LTL: определение и приведение к разделенной нормальной форме с условными обязательствами
(03.11.2007 - 17:30)

http://video.google.com/videoplay?docid=4644109771909488581
10. Разделенная нормальная форма для логики линейного времени LTL: условные обязательства и построение автомата
(04.11.2007 - 17:30)

http://video.google.com/videoplay?docid=777695514589470420
11. Автоматный подход
(04.11.2007 - 17:35)

http://video.google.com/videoplay?docid=-1252848972618758632
12. Проверка моделей ограниченной глубины
(04.11.2007 - 17:40)

http://video.google.com/videoplay?docid=4735165485716917506
13. Свидетельства и контрпримеры. Абстракция
(04.11.2007 - 17:45)

http://video.google.com/videoplay?docid=-521146122805026521
14. Заключение и чего же ожидать в экзамене
(04.11.2007 - 18:35)

http://video.google.com/videoplay?docid=-521146122805026521
Ваша оценка: Пусто Средняя: 4.2 (6 votes)
Share |
Курс "Верификация параллельных и распределенных программных систем"