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

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

2 Статистика ошибок Среднее количество ошибок на 1000 строк кода до тестирования 2 / 23

3 Причины ошибок Неправильное понимание задач Неправильное решение задач Неправильный перенос решений в код 3 / 23 ? !

4 Сложность программ Конференция NATO 1968 – software сложнее hardware Основная причина ошибок в ПО – его сложность 4 / 23

5 Сложность – большой размер 5 / 23

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

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

8 Сложность – запутанность int unknown_f(int x0, int x1) { if(x0 == 0) return x1; if(x1 == 0) return x0; if(x0>0 && x1 0) x1 = -x1; while(x1 != 0) { if(x1>x0 && x0>0 || x1

9 Борьба с ошибками Безошибочное программирование – Сильно ограничивается сложностью Автоматизация разработки – Повышает сложность возможных систем – Изменяет существенные источники ошибок Интеграция разработки и контроля качества – Нужны методы и инструменты контроля качества ПО Стандартизация – Нужны методы и инструменты проверки соответствия стандартам 9 / 23

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

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

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

13 Зачем нужна формальность? 13 / 23

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

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

16 Пример: описание и работа теста 16 / 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, 137, }; }

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

18 Пример работы DART 18 / 23 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

19 Counterexample guided abstraction refinement [E. M. Clarke & O. Grumberg et al 2000, T. Ball & S. K. Rajamani 2000] do { ;... if(*) {... ; } } while (*); Авто-уточнение моделей 19 / 23 do { nPacketsOld = nPackets;... if(request) {... nPackets++; } } while (nPackets != nPacketsOld); do { b = true;... if(*) {... b = b?false:*; } } while (!b);

20 Работы отдела ТП Разработка тестов и тестирование Информационная система оператора связи Операционные системы реального времени Базовые библиотеки Linux (Linux Standard Base) Протоколы IPv6, Mobile IPv6, IPsec Отдельные модули компиляторов Intel Микропроцессоры архитектуры MIPS Создание технологий и инструментов Тестирование на основе моделей (UniTESK) Проверка соответствия стандарту LSB Верификация драйверов Linux 20 / 23

21 Разработки и исследования 21 / 23

22 Карьера в ИСП РАН 22 / 23 студент разработчик преподаватель старший разработчик руководитель группы архитектор исследователь аспирант

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