Лекция 1. Введение в формальные методы проверки правильности программ (К. Савенков - Верификация программ на моделях (2012)), страница 2

невозможно составить достаточнодетальное конечное описание системы•  Решение: в систему добавляетсякомпонент, выполняющий–  мониторинг поведения системы,–  анализ наблюдаемого поведения,–  реакцию на обнаруженные нарушенияспецификацииДинамическая верификация•  Проверяется правильность не описанияпрограммы, а её наблюдаемогоповедения•  Примеры:–  Система контроля поведения приложений вОС–  Система обнаружения атак–  Встроенная система контроляИстория развития1: фундамент•  Флойд, 1967 – assertions, гипотеза одоказуемости корректности программы,•  Хоар, 1969 – пред- и пост-условия, триплетыХоара (P | S | Q), логический вывод,•  Бойер, Мур, 1971 – первый автоматическийпрувер,•  Дейкстра, 1975 – Guarded Command Languages,•  Хоар, 1978 – взаимодействующиепоследовательные процессы (CSP),•  Милнер, 1980 – Calculus of CommunicatingSystems (CCS)1VahePoladian, Software Technology Maturation Study: Model Checking Techniques and Tools, 2001.История развития: развитиеметодов•  Пнуэли, 1977 – темпоральная логика LTL,•  Пнуэли, 1981 – логика ветвящегося времени(CTL),•  Кларк, Эмерсон, 1981 и Квили, Сифакис, 1982 –model checking (обход достижимых состояний),•  Варди и Вольпер, 1986 – новая техника modelchecking (анализ конформности),•  Хольцман, 1989 – верификатор SPIN.?1981!?1986!История развития: проблема«комбинаторного взрыва»•  Бриан, 1989 – Двоичные решающиедиаграммы (BDD),•  МакМиллан, 1993 – верификатор SMV(символьная верификация, BDD),•  Хольцман, Пелед, 1994 – редукциячастичных порядков,•  1995 – редукция частичных порядковв SPIN.История развития: дальнейшееразвитие•  Кларк, 1992 – абстракция для уменьшениячисла состояний модели,•  Эльсаиди, 1994 – семантическаяминимизация,•  Пелед, 1996, Бир, 1998 – верификациямодели «на лету»,•  Равви, 2000 – анализ достижимости сучётом спецификации,•  Эмерсон, Прасад, 1994 – симметрияПлан лекции•  Правильность программ•  Актуальность верификации•  Формальные методы проверкиправильности•  Обзор курса•  ПрактикумПрограмма курса•  Практические знания:–  Оценка числа состояний программы,построение модели программы наPromela, спецификация свойствпрограммы, верификация при помощиSpin, анализ результатов верификации•  Теоретическая основа:–  Математическая модель программы(состояние, вычисление, системапереходов граф программы)–  Построение модели (абстракция)программы, вопросы её корректностиМатериалыСайт курса: http://savenkov.lvk.cs.msu.su/mc.htmlМатериалы по SPIN:• • Holzmann.

The Spin Model Checker: Primer andReference Manual, Addison Wesley, 2003.Сайт Spin: http://www.spinroot.com.Дополнительная литература:• • • • Кларк, Грумберг, Пелед. Верификация моделей программ: Modelchecking, МЦНМО, 2002.Peled. Software Reliability Methods, Springer, 2001.Миронов А.М. Верификация программ методом Model Checking.http://intsys.msu.ru/staff/mironov/modelchk.pdfМиронов А.М. Теория процессов http://intsys.msu.ru/staff/mironov/processes.pdfПрактикум• • • • • • Первое задание – 20.02;Ауд. 758, Linux, SPIN;5 задач, по мере прохождения курса;Экзамен – устный;посмотримE-mail: model-checking@lvk.cs.msu.su,Подписаться: отправить ФИО иномер группы наmodel-checking@lvk.cs.msu.su,•  Информация и задачи – по почте.Оценка за практикум и курс•  Курс ориентирован на получение знанийи навыков,•  Навыки не получится развить передэкзаменом и продемонстрировать за 20минут•  Оценка за курс:–  Оценка за практикум (0..3 балла),–  Оценка за экзамен (0..3 балла),–  Оценка за «летучки» (-1..1 балл).•  Для АСВК оценка за практикум идёт вдиплом.Оценка за практикум и курс•  5 задач: 50+100+50+80+100 = 380 очков–  [0,230) – 0 баллов (неуд по практикуму, недопуск наосновной экзамен),–  [230,300) – 1 балл,–  [300,380) – 2 балла,–  380 – 3 балла (кандидат на «автомат»);•  На занятиях можно сдавать сколько угодно раз,вплоть до получения максимального балла;•  Если решение задачи присылается по почте,оценка за него является окончательной;•  Сдача задания после дедлайна:–  в течение двух недель,–  только очная (на семинаре),–  оценка умножается на 0.6.Спасибо за внимание!.