Корректность и надежность программного обеспечения Состояние и тенденции Директор ИСП РАН академик Иванников В.П. ivan@ispras.ru. - презентация

1 Корректность и надежность программного обеспечения Состояние и тенденции Директор ИСП РАН академик Иванников В.П.

2 Рост размеров кода программных систем СистемаГодРазмер (10 6 LOC)Размер команды Windows Windows NT Windows NT Windows Windows XP Linux Kernel ,7 Open Solaris20059,7 Mac OS X Windows Vista2007> 50 Дистрибутив Debian Вся авионика США (бортовая и наземная) 2007~1000

3 Рост сложности по всем аспектам Эскалация размеров Увеличение функциональных возможностей Рост объемов перерабатываемых данных Расширение использования параллелизма и распределенности Рост требований к переносимости и совместимости Рост гетерогенности (использование в одной системе многих технологий и языков)

4 Статистика ошибок Количество ошибок на 1000 строк неоттестированного кода остается неизменным Программные системыЧисло ошибок на 1000 строк кода Среднее по индустрии (McConnell)15-50 Microsoft (до тестирования)10-20 NASA JPL (до тестирования)6-9 Linux~7 Microsoft (продукты)0.5 NASA JPL (продукты)0.003

5 Инциденты, связанные с дефектами в ПО Космические аппараты –Mariner I (1962) –Фобос-1 (1988) –Ariane 5 (1996) –Mars Climate Orbiter (1999) –Mars Polar Lander (1999) Коммуникации –AT&T network crash (1990) –OpenSSL rnd in Debian (2006-8) Транспорт –Heathrow Airport Terminal 5 baggage system (2008) –Toyota Prius (2005, 2010) Банки –Gemalt banking cards (2010) Медицинское оборудование – Therac-25 (1985-7) Энергетика – Northeast Blackout (2003) – Stuxnet worm (2010) Военное оборудование – Lockheed F-117 (1982) – MIM-104 Patriot (1991) – USS Yorktown (1997) – F-22 Raptor (2007) Потери индустрии США в 2001 году – ~ $ (оценка NIST)

6 Что делать? Методы проверки корректности –Экспертиза –Тестирование –Статический анализ –Формальные методы –Синтетические методы Предотвращение ошибок и снижение затрат на их исправление

7 Методы проверки корректности (1) Экспертиза (review, inspection) –Внимательно читаем код, моделируем возможные ситуации, анализируем получаемые свойства, выявляем неясные места, расхождения с требованиями –Обычно участвуют несколько человек (так гораздо эффективнее, но и труднее) –Невозможно автоматизировать –Очень высокая трудоемкость ~30-50 LOC/человек·час –Выявляется большая часть ошибок –Применяется для критически важных систем, требующих высокой надежности

8 Методы проверки корректности (2) Тестирование –Придумываем набор тестов-сценариев, выполняем систему на них, проверяем соответствие результатов требованиям –Выполнение часто автоматизируется –Низкая трудоемкость –Применимо для почти всех систем –Большинство ошибок находятся, но есть очень трудные категории (гонки) –Качество проверки зависит от набора тестов, придумывание хорошего набора нетривиально – зависит от конкретной задачи и технологий

9 Методы проверки корректности (3) Статический анализ –Выявляем шаблон ошибки, автоматизируем его поиск, анализируем список подозрительных мест –Хорошо автоматизируется, но результаты обычно анализируются человеком –Дилемма: либо анализ простой и быстрый, но выдает много ложных сообщений об ошибках, либо мусора мало, но анализ сложный и медленный –Эффективен для часто встречающихся ошибок (null pointer, переполнение буфера и пр.), особо эффективен для параллелизма (гонки, взаимоблокировки) –Почти не применим для смысловых ошибок

10 Методы проверки корректности (4) Формальные методы –Описываем систему и требования к ней формально и пытаемся установить соответствие между ними или найти расхождения –Очень трудоемко и нетривиально, требуется высокая математическая квалификация –Применяется для критически важных систем Два вида –Дедуктивный анализ (theorem proving) Логические или алгебраические формализмы –Проверка моделей (model checking) Требования – темпоральная логика, система – конечный автомат

11 Проверка моделей Возможность полной автоматизации –Либо доказываем корректность –Либо находим ошибку и получаем конкретный сценарий ее проявления –Либо ответ неопределен из-за сложности модели Бурный прогресс инструментов за 20 лет Эффективно обрабатываются модели до ~10 10 состояний, иногда больше (до ), но большая модель не может быть произвольной, она должна иметь очень мало нерегулярностей

12 Методы проверки корректности (5) Синтетические методы –Смешиваем несколько техник Например, извлекаем модель автоматически из кода, затем проводим проверку этой модели Например, строим формальную модель и используем ее для генерации тестов Например, извлекаем статическую структуру кода и генерируем тесты так, чтобы покрыть все ее элементы … –Активно развиваются последние 10 лет –3-4 промышленно применимые техники, но они дают новый уровень качества в ряде областей

13 Пример: тестирование на основе моделей Описываем систему как набор компонентов, каждый компонент – (расширенный) конечный автомат Генерируем тесты как набор путей, покрывающих все переходы всех автоматов Опыт ИСП РАН и Microsoft –Системы до ~10 6 строк –Документация до ~10 4 страниц –Высокое качество при приемлемой трудоемкости, но сложнее обычного тестирования –Разработчику тестов нужна дополнительная квалификация, создание тестов так же креативно, как разработка –Применимо для систем высокой надежности

14 Предотвращение и исправление ошибок Повышение уровня абстракции кода –Полностью устраняет некоторые виды ошибок Стандартизация и уточнение семантики языков, протоколов и интерфейсов –Формализация правил использования и обязательств Формальное моделирование и анализ на ранних этапах –Основная область применения формальных методов Перенос верификации и разработки тестов как можно ближе к началу кодирования (итеративность) – проверять как можно раньше, исправлять быстрее, действовать так для каждого отдельного компонента

15 Заключение Сложность программных систем постоянно растет По этой причине ошибки неизбежны Выявление ошибок –Традиционное: экспертиза, тестирование и статический анализ Широко применяются, но отстают по масштабируемости от технологий разработки –Более современное: синтетические методы Применяются пока реже, но иногда более масштабируемы