lect01 (К. Савенков - Верификация программ на моделях (2010))

PDF-файл lect01 (К. Савенков - Верификация программ на моделях (2010)) Надёжность программного обеспечения (53042): Лекции - 7 семестрlect01 (К. Савенков - Верификация программ на моделях (2010)) - PDF (53042) - СтудИзба2019-09-18СтудИзба

Описание файла

Файл "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 caBB  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 балл).• Для АСВК оценка за практикум идѐт вдиплом;• Если решение задачи присылается попочте, оценка за него являетсяокончательной.Спасибо за внимание!.

Свежие статьи
Популярно сейчас
А знаете ли Вы, что из года в год задания практически не меняются? Математика, преподаваемая в учебных заведениях, никак не менялась минимум 30 лет. Найдите нужный учебный материал на СтудИзбе!
Ответы на популярные вопросы
Да! Наши авторы собирают и выкладывают те работы, которые сдаются в Вашем учебном заведении ежегодно и уже проверены преподавателями.
Да! У нас любой человек может выложить любую учебную работу и зарабатывать на её продажах! Но каждый учебный материал публикуется только после тщательной проверки администрацией.
Вернём деньги! А если быть более точными, то автору даётся немного времени на исправление, а если не исправит или выйдет время, то вернём деньги в полном объёме!
Да! На равне с готовыми студенческими работами у нас продаются услуги. Цены на услуги видны сразу, то есть Вам нужно только указать параметры и сразу можно оплачивать.
Отзывы студентов
Ставлю 10/10
Все нравится, очень удобный сайт, помогает в учебе. Кроме этого, можно заработать самому, выставляя готовые учебные материалы на продажу здесь. Рейтинги и отзывы на преподавателей очень помогают сориентироваться в начале нового семестра. Спасибо за такую функцию. Ставлю максимальную оценку.
Лучшая платформа для успешной сдачи сессии
Познакомился со СтудИзбой благодаря своему другу, очень нравится интерфейс, количество доступных файлов, цена, в общем, все прекрасно. Даже сам продаю какие-то свои работы.
Студизба ван лав ❤
Очень офигенный сайт для студентов. Много полезных учебных материалов. Пользуюсь студизбой с октября 2021 года. Серьёзных нареканий нет. Хотелось бы, что бы ввели подписочную модель и сделали материалы дешевле 300 рублей в рамках подписки бесплатными.
Отличный сайт
Лично меня всё устраивает - и покупка, и продажа; и цены, и возможность предпросмотра куска файла, и обилие бесплатных файлов (в подборках по авторам, читай, ВУЗам и факультетам). Есть определённые баги, но всё решаемо, да и администраторы реагируют в течение суток.
Маленький отзыв о большом помощнике!
Студизба спасает в те моменты, когда сроки горят, а работ накопилось достаточно. Довольно удобный сайт с простой навигацией и огромным количеством материалов.
Студ. Изба как крупнейший сборник работ для студентов
Тут дофига бывает всего полезного. Печально, что бывают предметы по которым даже одного бесплатного решения нет, но это скорее вопрос к студентам. В остальном всё здорово.
Спасательный островок
Если уже не успеваешь разобраться или застрял на каком-то задание поможет тебе быстро и недорого решить твою проблему.
Всё и так отлично
Всё очень удобно. Особенно круто, что есть система бонусов и можно выводить остатки денег. Очень много качественных бесплатных файлов.
Отзыв о системе "Студизба"
Отличная платформа для распространения работ, востребованных студентами. Хорошо налаженная и качественная работа сайта, огромная база заданий и аудитория.
Отличный помощник
Отличный сайт с кучей полезных файлов, позволяющий найти много методичек / учебников / отзывов о вузах и преподователях.
Отлично помогает студентам в любой момент для решения трудных и незамедлительных задач
Хотелось бы больше конкретной информации о преподавателях. А так в принципе хороший сайт, всегда им пользуюсь и ни разу не было желания прекратить. Хороший сайт для помощи студентам, удобный и приятный интерфейс. Из недостатков можно выделить только отсутствия небольшого количества файлов.
Спасибо за шикарный сайт
Великолепный сайт на котором студент за не большие деньги может найти помощь с дз, проектами курсовыми, лабораторными, а также узнать отзывы на преподавателей и бесплатно скачать пособия.
Популярные преподаватели
Нашёл ошибку?
Или хочешь предложить что-то улучшить на этой странице? Напиши об этом и получи бонус!
Бонус рассчитывается индивидуально в каждом случае и может быть в виде баллов или бесплатной услуги от студизбы.
Предложить исправление
Добавляйте материалы
и зарабатывайте!
Продажи идут автоматически
5057
Авторов
на СтудИзбе
456
Средний доход
с одного платного файла
Обучение Подробнее