Надёжность ПО (All in one) (2014)

НАДЁЖНОСТЬ ПРОГРАММНОГО ОБЕСПЕЧЕНИЯЛекция 1:Введение в разработку надёжного ПОВМиК МГУ им. М.В. Ломоносова,Кафедра АСВК, Лаборатория Вычислительных КомплексовАссистент Волканов Д.Ю.Краткий план лекций• Как избежать следующих ситуаций:2План лекции••••Введение в курсНадёжность ПОРазработка надёжного ПОВведение в процесс разработкинадёжного ПО3О чём этот курс• Концепции и связи• Аналитические модели и средстваподдержки• Методы для увеличения надёжности ПО:––––––ВерификацияСтатический анализТестированиеРасчёт надёжностиАнализ статистики ошибокБезопасность4Как это сдавать• В январе экзамен• В процессе семестра с/р– 80% - 100% -> автоматом 5– 60% - 79,9% -> 4– 40% - 59,9% -> 3– 20% - 39,9% -> 2– 0% - 19,9% -> 1– экзамен письменноустный5Практикум• Несколько заданий, по мерепрохождения курса• Первое задание – 16.09• Умение работать в программныхсредствах• Каждое задание - 10 баллов• Каждая неделя сверхДедлайна –N задания6Неисправность, ошибка,отказ7Пример, поясняющий понятиеотказаProgram definitions;var s:integer;beginread(s);s:=s*2; {неисправность}L: {ошибка}s:=s mod 5;write(s); {отказ}end.Ожидаемые Текущиеданныеданные663612361212128Разработка программыАнал Проект Реалиро- иизвани зациеяВнесённыеошибкиОбнаруженныеошибкиТестированиеUni SysttemЭксплуатацияЦенаошибки9Правильность программ• Нет требований – нет правильности• Ошибка – несоответствие требованиям• Ошибки:– в формулировке требований,building the wrong system,– в соблюдении требований,building the system wrong.10Правильность программ• Валидация – исследование и обоснование того,что спецификация ПО и само ПО черезреализованную в нём функциональностьудовлетворяет требованиям пользователей,• Верификация – исследование и обоснованиетого, что программа соответствует своейспецификации.найти ошибки или доказать, что их нетNB: ошибки формализации требований11Цена ошибки• В ряде приложений ошибки некритичны:– сводятся к лёгким моральным травмам,– возможность обнаружения сбоя ивосстановления,– возможность быстрого исправленияошибки.12Цена ошибки• Системы с повышеннымитребованиями к надёжности (Safetycritical)• Ошибки приводят к:– Гибели или травмам людей,– Крупным финансовым потерям– Ущербу окружающей среде– Итд.13Цена ошибки: Ariane-5• Июнь 1996 года, взрыв ракеты спустя40 сек.

после старта,• Ущерб – $500млн (разработка – $7млрд.),• Причина – 64bit float -> 16bit int.14Цена ошибки: Patriot• Февраль 1991 года, Patriotпромахнулся мимо ракеты Scud,• Ущерб – 28 убитых, >100 раненых,• Причина – ошибка округления из-за24bit fixed, Scud успел пролететь500м.15Цена ошибки: Sleipner A• август 1991 года, Северное море, платформаSleipner A затонула после разрушенияоснования,• Ущерб – $700 млн, землетрясение силой 3балла,• Причина – ошибка округления примоделировании платформы.16Кое-что посвежее (2010)•Ошибки в ПО автомобилей: Toyota Prius (нарушен директивныйинтервал включения ABS), Chrysler (можно вытащить ключ, непереключившись в режим парковки)• Ошибки в программе обработки заявлений доноров органов вUK (у 25 человек взяли не те органы)• Ошибка в электронной системе налоговой службы США (необслуживались 64-летние люди)• Ошибка в антивирусе McAfee (системный файл Windowsраспознан как вредоносный и удалён, бесконечный ребут)• Отключение Skype (вышла из строя одна из версий клиента, чтопривело к сбою всей P2P сети)• Ошибка в апдейте NYSE Euronext (S&P упал на 10%)• 88 критических ошибок в Android Froyo (доступ к личнымданным)17Повышенные требования кнадежности• Не только спутники, самолёты и АЭС!• Системы, в которых– затруднено исправление ошибок (потребительскаяэлектроника)– велик масштаб использования (та же электроника,важные веб-сервисы)– высокая степень доверия человека (augmentedreality)• Критически-важных систем становитсявсё больше, они становятся болеесложными и интероперабельными.18Выборочное тестирование«Тестирование может показать присутствие ошибок,но не может показать их отсутствия» (с) Дейкстра.Выявление ошибокчастыебезвредныекритическиетестированиередкиеневажноформальныеметоды19ReminderВЕРИФИКАЦИЯ ПРОГРАММЫ ВОБЩЕМ СЛУЧАЕАЛГОРИТМИЧЕСКИНЕРАЗРЕШИМАСм., например, задачу останова программы,теорему Райса, etc20Формальные методы«Использование математического аппарата,реализованного в языках, методах и средствахспецификации и верификации программ»•Методы формальной спецификации•Методы формальной верификации:– Доказательство теорем– Верификация на моделях– Кое-что ещё21Методы верификации••••••«Полное» тестированиеИмитационное моделированиеДоказательство теоремСтатический анализВерификация на моделяхДинамическая верификация22Тестирование• Обоснование полноты тестовогопокрытия,• Метод «чёрного ящика» (ЧЯ) -полное покрытие входных данных,• Метод «прозрачного ящика» (ПЯ) -полное покрытие кода программы.23Тестирование: плюсы• Проверяется та программа, котораябудет использоваться,• Не требуется (знания)дополнительных инструментальныхсредств,• Удобная локализация ошибки.24Тестирование: минусы• Не всегда есть условия длятестирования системы,• Проблема с воспроизводимостьютестов.частичное решение –имитационное моделирование25Тестирование: подводныекамни• Полнота тестового покрытия:– ЧЯ: для последовательных программ сложноперебрать все входные данные,– ЧЯ: для параллельных – очень сложно,– ЧЯ: для динамических структур данных,взаимодействия с окружением – невозможно.– ПЯ: большой размер покрытия,– ПЯ: часто невозможно построить 100%покрытие,– ПЯ: полное покрытие не гарантируетотсутствия ошибок.26Полное покрытие длячерного ящика• Поиск выигрышной стратегии вшашках:– 1014 тестов,– 18 лет,– постоянно работало от 50 до 200десктопов.27Полное покрытие дляпрозрачного ящикаif (B1) {S1;}if (B1) {S1;}if (B2) {S2;}- Два теста- Четыре теста…exp…28Полное покрытие дляпрозрачного ящикаint x = 1;if (x== 1){std::cout“Okay” << std::endl;<<} else {std::cout << “Error” << std::endl;}-- полное покрытие кода невозможно29Полное тестовое покрытие – непанацеяint strlen(const char* p) { intlen = 0;do {++len;}while(*p++); return len;}«а», «bbb» -- полное покрытие кода,ошибка не найдена30Полнота покрытия: итоги• Полный перебор входных данных –невозможен, плохой критерий,• Полнота покрытия кода – не гарантируетправильности, плохой критерий,• Ошибка – ошибочное вычисление системы,• Полнота в терминах возможныхвычислений – хороший критерий.31Кое-что о тестировании• Как правило, разработка критически важныхсистем регулируется каким-либо стандартом;Например, RTCA/DO-178B (авионика);• Стандарты разрабатывались давно, поэтомуосновной способ верификации там –тестирование;• Пример обоснования полноты тестового покрытиядля критических систем – MC/DC (http://techreports.larc.nasa.gov/ltrs/PDF/2001/tm/NASA-2001-tm210876.pdf);• В стандарт RTCA/DO-178C (2011г) включеныmodel-driven development и верификация32Дополнительные трудности:Реактивные программы• Традиционные программы:– Завершаются,– Описание «вход/выход»,– Число состояний зависит от входныхданных и переменных;• Реактивные программы:–––––Работают в бесконечном цикле,Взаимодействуют с окружением,Описание «стимул/реакция»,(Не обязательно параллельные),Дополнительный источник сложности.33Дополнительные трудности:Параллельные программы••••Большое количество возможных вычислений,Неочевидные ошибки,Пример – системы с разделением ресурсов.Исключительная ситуация:• Правила, реализованные в программах, должныбыть универсальны34Системы с разделениемресурсовПримеры:• Дорожный траффик,• Телефонные сети,• Операционные системы,•…35Дополнительные трудности:Параллельные системы• Новый источник ошибок – совместнаяработа проверенных компонентов,• Невоспроизводимость тестов,• Ограниченные возможности понаблюдению.36Доказательство теорем• Система и свойства – формулы• Набор аксиом и правил вывода• Строится доказательство свойстватеоремы• Качественный анализ системы37Доказательство теорем• Система:AcaBBbA• Свойство:ac?• Правила вывода:S1  a1  S2  S2  a2  S3 s1  s2  s2  s3,S1  a1  a2  S3s1  s338Доказательство теорем• Достоинства:– работа с бесконечными пр-вами состояний,– даёт более глубокое понимание системы.• Недостатки:– медленная скорость работы,– может потребоваться помощь человека(построение инвариантов циклов),– В общем случае нельзя построить полнуюсистему аксиом и правил вывода (теореманеполноты Гёделя).39Статический анализ• Более грубый и прагматичныйподход,• Анализ исходного текста программыбез её выполнения,• В общем случае задача неразрешима(сводится к анализу достижимости операторапрограммы),• Поиск компромисса междупотребностями и возможностями.40Статический анализ• Абстрактная интерпретация: построениеабстрактной семантики языка программированияи интерпретация текста программы всоответствии с этой семантикой,• В случае тестирования: проверяем, чтоконкретные вычисления программы не приводятеё в ошибочные состояниясостояниевремя41Статический анализ• Абстрактная интерпретация: построениеабстрактной семантики языка программирования иинтерпретация текста программы в соответствии сэтой семантикой,• Статический анализ: аппроксимируем «сверху»множество вычислений программы,• Возможны ложные сообщения о нарушении свойств!состояниевремя42Статический анализ: примерПроверка инициализированности переменной:43Статический анализ: примерПроверка инициализированности переменной:44Статический анализ• Достоинства– Высокая скорость работы,– Если ответ дан, ему можно верить.• Недостатки– Узкая область применения (оптимизацияв компиляторах, анализ похожести кода,анализ безопасности итп.),– Ручная настройка при изменениипроверяемых свойств45Верификация программ намоделях (model checking)• Проверка свойства на конечноймодели программы,• Свойства – в терминах значенияпредикатов в состоянии программы ипоследовательности значений.• Исчерпывающий поиск попространству состояний.46Верификация программ намоделях: пример47Верификация программ намоделях: пример• Модель функции count_lines:f = NULLentryfopenopenedfcloseclosedreturnexitferror(f) = 148Процесс верификациипрограмм на моделях• Моделирование– Построить адекватную и корректную модель,– Избежать «лишних» состояний;• Спецификация свойств– Темпоральная логика,– Полнота свойств;• Верификация– Построение контрпримера,– Анализ контрпримера.49Верификация программ намоделях• Достоинства– Хорошо автоматизируем,– Если модель конечна, корректна иадекватна проверяемому свойству, тодаётся точный ответ,– Выявляет редкие ошибки.• Недостатки– Работает только для конечныхмоделей.50Динамическая верификация• Иногда на этапе разработки системыневозможно гарантировать еёправильную работу в ходе эксплуатации:– Динамическое изменение конфигурациисистемыпример: компьютерная сеть– Неполное описание компонентов системыпример: мультивендорная система– Работа в сложном окружениипример: взаимодействие с Интернет51Динамическая верификация• Т.е.