lect01 (К. Савенков - Верификация программ на моделях (2010))
Описание файла
Файл "lect01" внутри архива находится в папке "К. Савенков - Верификация программ на моделях (2010)". PDF-файл из архива "К. Савенков - Верификация программ на моделях (2010)", который расположен в категории "". Всё это находится в предмете "надёжность программного обеспечения" из 7 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст из PDF
Верификация программна моделяхКонстантин Савенков (лектор)План лекции• Правильность программ• Актуальность верификации• Формальные методы проверкиправильности• Обзор курса• ПрактикумРазработка программыАнализПроектированиеРеализацияВнесѐнныеошибкиОбнаруженныеошибкиТестированиеUnitSystemЦенаошибкиЭксплуатацияПравильность программ• Нет требований – нет правильности• Ошибка – несоответствие требованиям• Ошибки:– в формулировке требований,building the wrong system,– в соблюдении требований,building the system wrong.Правильность программ• Валидация– исследование и обоснование того,что спецификация ПО и само ПО черезреализованную в нѐм функциональностьудовлетворяет требованиям пользователей,• Верификация– исследование и обоснованиетого, что программа соответствует своейспецификации.найти ошибки или доказать, что их нетЦена ошибки• Системы с повышеннымитребованиями к надѐжности (Safetycritical)• Ошибки приводят к:– Гибели или травмам людей,– Крупным финансовым потерям– Ущербу окружающей среде– Итд.Цена ошибки: Ariane-5• Июнь 1996 года, взрыв ракеты спустя40 сек.
после старта,• Ущерб – $500млн (разработка – $7млрд.),• Причина – 64bit float -> 16bit int.Цена ошибки: Patriot• Февраль 1991 года, Patriotпромахнулся мимо ракеты Scud,• Ущерб – 28 убитых, >100 раненых,• Причина – ошибка округления из-за24bit fixed, Scud успел пролететь500м.Цена ошибки: Sleipner A• август 1991 года, Северное море, платформаSleipner A затонула после разрушенияоснования,• Ущерб – $700 млн, землетрясение силой 3балла,• Причина – ошибка округления примоделировании платформы.Выборочное тестирование«Тестирование может показать присутствие ошибок,но не может показать их отсутствия» (с) Дейкстра.Выявление ошибокчастыебезвредныекритическиетестированиередкиеневажноформальныеметодыReminderВЕРИФИКАЦИЯ ПРОГРАММЫВ ОБЩЕМ СЛУЧАЕАЛГОРИТМИЧЕСКИ НЕРАЗРЕШИМАСм., например, задачу останова программы,теорему Райса, etcФормальные методы«Использование математического аппарата,реализованного в языках, методах и средствахспецификации и верификации программ»• Методы формальной спецификации• Методы формальной верификации:– Доказательство теорем– Верификация на моделях– Кое-что ещѐМетоды верификации••••••«Полное» тестированиеИмитационное моделированиеДоказательство теоремСтатический анализВерификация на моделяхДинамическая верификацияТестирование• Обоснование полноты тестовогопокрытия,• Метод «чѐрного ящика» (ЧЯ) -полное покрытие входных данных,• Метод «прозрачного ящика» (ПЯ) -полное покрытие кода программы.Тестирование: плюсы• Проверяется та программа, котораябудет использоваться,• Не требуется (знания)дополнительных инструментальныхсредств,• Удобная локализация ошибки.Тестирование: минусы• Не всегда есть условия длятестирования системы,• Проблема с воспроизводимостьютестов.частичное решение –имитационное моделированиеТестирование: минусы• Полнота тестового покрытия:– ЧЯ: для последовательных программ сложноперебрать все входные данные,– ЧЯ: для параллельных – очень сложно,– ЧЯ: для динамических структур данных,взаимодействия с окружением – невозможно.– ПЯ: большой размер покрытия,– ПЯ: часто невозможно построить 100%покрытие,– ПЯ: полное покрытие не гарантируетотсутствия ошибок.Полное покрытие длячерного ящика• Поиск выигрышной стратегии вшашках:– 1014 тестов,– 18 лет,– постоянно работало от 50 до 200десктопов.Полное покрытие дляпрозрачного ящикаif (B1) {S1;}if (B1) {S1;}if (B2) {S2;}- Два теста- Четыре теста…exp…Полное покрытие дляпрозрачного ящикаint x = 1;if (x == 1) {std::cout << “Okay” << std::endl;} else {std::cout << “Error” << std::endl;}-- полное покрытие кода невозможноПолное тестовое покрытие – непанацеяint strlen(const char* p) {int len = 0;do {++len;} while (*p++);return len;}«а», «bbb» -- полное покрытие кода,ошибка не найденаПолнота покрытия: итоги• Полный перебор входных данных –невозможен, плохой критерий,• Полнота покрытия кода – не гарантируетправильности, плохой критерий,• Ошибка – ошибочное вычисление системы,• Полнота в терминах возможныхвычислений – хороший критерий.Кое-что о тестировании• Как правило, разработка критически важныхсистем регулируется каким-либо стандартом;Например, RTCA/DO-178B (авионика);• Стандарты разрабатывались давно, поэтомуосновной способ верификации там –тестирование;• Пример обоснования полноты тестового покрытиядля критических систем – MC/DC(http://techreports.larc.nasa.gov/ltrs/PDF/2001/tm/NASA-2001-tm210876.pdf).Реактивные программы• Традиционные программы:– Завершаются,– Описание «вход/выход»,– Число состояний зависит от входныхданных и переменных;• Реактивные программы:–––––Работают в бесконечном цикле,Взаимодействуют с окружением,Описание «стимул/реакция»,(Не обязательно параллельные),Дополнительный источник сложности.Реактивные программы••••Большое количество возможных вычислений,Неочевидные ошибки,Пример – системы с разделением ресурсов.Исключительная ситуация:• Правила, реализованные в программах, должныбыть универсальныСистемы с разделениемресурсовПримеры:• Дорожный траффик,• Телефонные сети,• Операционные системы,•…Параллельные системы• Новый источник ошибок – совместнаяработа проверенных компонентов,• Невоспроизводимость тестов,• Ограниченные возможности понаблюдению.Доказательство теорем• Система и свойства – формулы• Набор аксиом и правил вывода• Строится доказательство свойстватеоремы• Качественный анализ системыДоказательство теорем• Система:A caBB b Aa c?• Свойство:• Правила вывода:S1 a1 S2 S2 a2 S3 s1 s2 s2 s3,S1 a1 a2 S3s1 s3Доказательство теорем• Достоинства:– работа с бесконечными пр-вами состояний,– даѐт более глубокое понимание системы.• Недостатки:– медленная скорость работы,– может потребоваться помощь человека(построение инвариантов циклов),– В общем случае нельзя построить полнуюсистему аксиом и правил вывода (теореманеполноты Гѐделя).Доказательство теорем• Примеры инструментальных средств:– Isabelle/HOL, Coq, PVS, Vampire, SPASS, ACL2, Simplify,Microsoft Z• Что почитать:– ATP было в курсе «Математическая логика» В.А.Захарова– Xavier Leroy, Mechanized semantics with applications toprogram proof and compiler verification, INRIA, France,2009 (http://pauillac.inria.fr/~xleroy/courses/Marktoberdorf2009/notes.pdf)– О PVS расскажут на 5-м курсеСтатический анализ• Более грубый и прагматичныйподход,• Анализ исходного текста программыбез еѐ выполнения,• В общем случае задача неразрешима(сводится к анализу достижимости операторапрограммы),• Поиск компромисса междупотребностями и возможностями.Статический анализ• Абстрактная интерпретация: построениеабстрактной семантики языка программированияи интерпретация текста программы всоответствии с этой семантикой,• В случае тестирования: проверяем, чтоконкретные вычисления программы не приводятеѐ в ошибочные состояниясостояниевремяСтатический анализ• Абстрактная интерпретация: построениеабстрактной семантики языка программирования иинтерпретация текста программы в соответствии сэтой семантикой,• Статический анализ: аппроксимируем «сверху»множество вычислений программы,• Возможны ложные сообщения о нарушении свойств!состояниевремяСтатический анализ: примерПроверка инициализированности переменной:int min(int* arr, int n) {int m;if (n > 0) {m = arr[0];}int i = 0;while (i < n) {if (m > arr[i]) {m = arr[i];}i++;}return m;}dom(m) = Int + { ω }NI = { ω }I = Intv: Expr -> {NI, I}Статический анализ: примерПроверка инициализированности переменной:int min(int* arr, int n) {int m;<v = { NI }>if (n > 0)<v = { NI }> {m = arr[0]; <v = { I }>} <v = { NI, I }> (!)int i = 0; <v = { NI, I }>while (i < n) <v = { NI, I }> {if (m > arr[i]) <v = { NI, I }> {m = arr[i]; <v = { I }>}i++; <v = { NI, I }>}return m; <v = { NI, I }>}dom(m) = Int + { ω }NI = { ω }I = Intv: Expr -> {NI, I}Статический анализ• Достоинства– Высокая скорость работы,– Если ответ дан, ему можно верить.• Недостатки– Узкая область применения (оптимизацияв компиляторах, анализ похожести кода,анализ безопасности итп.),– Ручная настройка при изменениипроверяемых свойствСтатический анализ• Примеры средств:– ASTREE (http://www.astree.ens.fr ),• Что почитать:– Reps, T., Program analysis via graphreachability.
Information and Software Technology 40,11-12 (November/December 1998), pp. 701-726.– P. Cousot & R. CousotA gentle introduction to formal verification of computersystems by abstract interpretation, Logics andLanguages for Reliability and Security, 2010, NATOScience Series III: Computer and Systems Sciences,IOS Press, 29 pages.Верификация программ намоделях (model checking)• Проверка свойства на конечноймодели программы,• Свойства – в терминах значенияпредикатов в состоянии программы ипоследовательности значений.• Исчерпывающий поиск попространству состояний.Верификация программ намоделях: примерint count_lines(const char* filename) {int c, count = 0;FILE* f = fopen(filename, "r");if (f != NULL) {c = fgetc(f);while (c != EOF) {if (c == '\n') {++count;}c = fgetc(f);}if (ferror(f)) {return -1;}fclose(f);return count;} else {return -1;}}Всегда лифункциязакрываетоткрытыйфайл?Верификация программ намоделях: пример• Модель функции count_lines:f = NULLentryfopenopenedfcloseclosedreturnferror(f) = 1exitПроцесс верификациипрограмм на моделях• Моделирование– Построить адекватную и корректную модель,– Избежать «лишних» состояний;• Спецификация свойств– Темпоральная логика,– Полнота свойств;• Верификация– Построение контрпримера,– Анализ контрпримера.Верификация программ намоделях• Достоинства– Хорошо автоматизируем,– Если модель конечна, корректна иадекватна проверяемому свойству, тодаѐтся точный ответ,– Выявляет редкие ошибки.• Недостатки– Работает только для конечных моделей.Динамическая верификация• Иногда на этапе разработки системыневозможно гарантировать еѐправильную работу в ходе эксплуатации:– Динамическое изменение конфигурациисистемыпример: компьютерная сеть– Неполное описание компонентов системыпример: мультивендорная система– Работа в сложном окружениипример: взаимодействие с ИнтернетДинамическая верификация• Т.е.
невозможно составить достаточнодетальное конечное описание системы• Решение: в систему добавляетсякомпонент, выполняющий– мониторинг поведения системы,– анализ наблюдаемого поведения,– реакцию на обнаруженные нарушенияспецификацииДинамическая верификация• Проверяется правильность не описанияпрограммы, а еѐ наблюдаемогоповедения• Примеры:– Система контроля поведения приложений вОС– Система обнаружения атак– Встроенная система контроляПрограмма курса• Практические знания:– Оценка числа состояний программы,построение модели программы наPromela, спецификация свойствпрограммы, верификация при помощиSpin, анализ результатов верификации• Теоретическая основа:– Математическая модель программы(состояние, вычисление, системапереходов граф программы)– Построение модели (абстракция)программы, вопросы еѐ корректностиЛитература•••••Сайт курса:http://savenkov.lvk.cs.msu.su/mc.htmlКларк, Грумберг, Пелед.
Верификациямоделей программ: Model checking,МЦНМО, 2002.Holzmann. The Spin Model Checker: Primerand Reference Manual, Addison Wesley,2003.Peled. Software Reliability Methods,Springer, 2001.Сайт Spin: http://www.spinroot.com.Практикум•••••Ауд. 758, Linux, SPIN;6 задач, по мере прохождения курса;Экзамен – устный;E-mail: model-checking@lvk.cs.msu.su,Подписаться: отправить ФИО иномер группы наmodel-checking@lvk.cs.msu.su,• Информация и задачи – по почте.Оценка за практикум и курс• Оценка за курс:– Оценка за практикум (0..3 балла),– Оценка за экзамен (0..3 балла),– Оценка за «летучки» (-1..1 балл).• Для АСВК оценка за практикум идѐт вдиплом;• Если решение задачи присылается попочте, оценка за него являетсяокончательной.Спасибо за внимание!.