Корректность программ Классические и современные подходы В. В. Кулямин Институт системного программирования РАН. - презентация

1 Корректность программ Классические и современные подходы В. В. Кулямин Институт системного программирования РАН

2 Корректные программы public int gcd(int x, int y) { int t; while(y != 0) { t = y; y = x%y; x = t; } return (x >= 0)?x:-x; } 2 / 22 gcd : int int int gcd(x,y) 0 gcd(x,y)|x gcd(x,y)|y z z|x z|y z|gcd(x,y) Спецификация

3 Размер программных систем 3 / 22

4 Ошибки и их причины Среднее количество ошибок на 1000 строк кода (до тестирования) 4 / 22 Основная причина ошибок в ПО – его сложность

5 Сложность задач и интерфейса 5 / 22

6 Сложность данных 6 / 22

7 Много компонентов 7

8 8 Сложность поведения

9 Много вариантов 9

10 Множество технологий 10

11 Риски, связанные с ошибками Космические аппараты Mariner I (1962) Фобос-1 (1988) Ariane 5 (1996) Mars Climate Orbiter (1999) Инфраструктура AT&T long distance network crash (1990) Northeast Blackout (2003) OpenSSL rnd in Debian (2006-8) Heathrow Airport Terminal 5 baggage system (2008) Банковские карты Gemalt (2010) Автомобили Toyota Prius (2005, 2010) Медицинское оборудование Therac-25 (1985-7) Medtronic Maximo (2008) Авионика и военное оборудование Lockheed F-117 (1982) MIM-104 Patriot (1991) Chinook ZD576 (1994) USS Yorktown (1997) F-22 Raptor (2007) 11 / 22

12 Что делать? Не делать ошибок – Невозможно из-за сложности Предотвращение ошибок – Тщательный анализ требований и возможных решений – Изоляция компонентов – Повышение уровня абстракции языков – Устранение error-prone конструкций – Стандартизация и документирование языков, библиотек, протоколов – Улучшение сопровождаемости, использование образцов, Выявление ошибок – Анализ свойств ПО – Контроль качества ПО 12 / 22

13 Контроль качества ПО Экспертиза (review, inspection) Статический анализ Проверка правил корректности Поиск конкретных ошибок по шаблонам Динамический анализ Мониторинг Тестирование Формальная верификация Дедуктивный анализ Проверка моделей Гибридные методы 13 / 22

14 Статика и динамика Статический анализ Динамический анализ 14 / 22 ТребованияИсходный код Инструмент анализа Требования Работа системы Среда мониторинга Создание тестов Пользователи

15 Формальная верификация Дедуктивный анализ [R. Floyd 1967, C. A. R. Hoare 1969] Логика Хоара – {Pre} Program {Post} Правила вывода Проверка моделей [E. M. Clarke & E. A. Emerson 1980, J. P. Queille & J. Sifakis 1982] Анализ достижимых состояний 15 / 22

16 Гибридные методы Интегрируют элементы различных подходов Тестирование на основе моделей Расширенный статический анализ Формальный мониторинг Синтетическое структурное тестирование Вспомогательные техники Символическое исполнение Абстрактная интерпретация Вывод ограничений Разрешение ограничений Автоматическое уточнение моделей 16 / 22

17 Тестирование на основе моделей 17 / 22 Оракул Тестируемая система Модель поведения Генератор воздействий Метрика полноты 12% Критерий полноты 36%57%87% Контроль корректности Контроль тщательности

18 Пример: описание теста 18 / public class AccountTest { Account public int getBalance() { return = = "bound) public void testDeposit(int x) { = "sums") public void testWithdraw(int x) { account.withdraw(x); } public boolean bound() { return getBalance() < 500; } public int[] sums = new int[]{0, 1, 2, 5}; }

19 Синтетическое тестирование DART [P. Godefroid, G. Agha, K. Sen 2005] 19 / 22 Исполнение Программа Символическое исполнение Поиск новых путей Тесты

20 Пример работы DART 20 / 22 int unknown_f(int x0, int x1) { if(x0 == 0) return x1; if(x1 == 0) return x0; if(x0>0 && x1x0 && x0>0 || x1x0 && x0 >0 || x10 && x1 0) && !(x1>x0 && x0>0 || x1

21 Работы отдела технологий программирования Разработка тестов и тестирование Информационная система оператора связи Операционные системы реального времени Базовые библиотеки ОС (POSIX, LSB) Протоколы IPv6, Mobile IPv6, IPsec Микропроцессоры архитектуры MIPS Система аварийной эвакуации пилота Компоненты компиляторов Intel, JDK, DOM API Технологии и инструменты Тестирование на основе моделей (UniTESK) Проверка соответствия стандарту LSB Верификация драйверов Linux Инструменты работы с требованиями Инструменты проектирования и конфигурирования авионики 21 / 22

22 22 / 22 Спасибо за внимание! Вопросы?

23 Общие книги по тестированию 23 / 22 B. Beizer. Software Testing Techniques. Thomson Computer Press, 1990 R. Binder. Testing Object-Oriented Systems: Models, Patterns, and Tools. Addison-Wesley, 2000 P. Ammann, J. Offutt. Introduction to software testing. Cambridge University Press, 2008.

24 Книги на русском языке Г. Майерс. Искусство тестирования программ. Финансы и статистика, 1982 Д. Месарош. Шаблоны тестирования xUnit. Рефакторинг кода тестов. Вильямс, 2009 Курс лекций 24 / 22

25 Модульное тестирование J.B.Rainsberger. JUnit Recipes. Practical Methods for Programmer Testing. Manning, 2005 C. Beust, H. Suleiman. Next Generation Java Testing. TestNG and Advanced Concepts. Addison- Wesley, / 22

26 Тестирование на базе моделей 26 / 22 M. Utting, B. Legeard. Practical Model-Based Testing. A Tools Approach. Morgan Kaufmann, 2006 J. Jacky, M. Veanes, C. Campbell, W. Schulte. Model Based Analysis and Testing with C#. Cambridge University Press, 2007

27 Теория тестирования M. Broy, B. Jonsson, J.-P. Katoen, M. Leucker, A. Pretschner, editors. Model Based Testing of Reactive Systems. Advanced Lectures. LNCS 3472, Springer, / 22