'

Корректность программ

Понравилась презентация – покажи это...





Слайд 0

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


Слайд 1

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


Слайд 2

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


Слайд 3

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


Слайд 4

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


Слайд 5

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


Слайд 6

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


Слайд 7

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


Слайд 8

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


Слайд 9

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


Слайд 10

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


Слайд 11

Формальная верификация Дедуктивный анализ [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


Слайд 12

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


Слайд 13

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


Слайд 14

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


Слайд 15

Пример: описание и работа теста 16 / 23 @Test public class AccountTest { Account account; @State public int getBalance() { return account.getBalance(); } @Test @DataProvider(name = "sums") @Guard(name = "bound“) public void testDeposit(int x) { account.deposit(x); } @Test @DataProvider(name = "sums") public void testWithdraw(int x) { account.withdraw(x); } public boolean bound() { return getBalance() < 500; } public int[] sums = new int[]{0, 1, 137, 1000000}; }


Слайд 16

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


Слайд 17

Пример работы DART 18 / 23 int unknown_f(int x0, int x1) { if(x0 == 0) return x1; if(x1 == 0) return x0; if(x0>0 && x1<0 || x0<0 && x1>0) x1 = -x1; while(x1 != 0) { if(x1>x0 && x0>0 || x1<x0 && x0<0) { x0 = x1-x0; x1 = x1-x0; x0 = x0+x1; } x1 = x0-x1; x0 = x0-x1; }   return x0; } x0 x1 Ограничение 0 0 !(x0 = 0) !(x0 = 0) && !(x1 == 0) !(x0 = 0) && !(x1 == 0) && !(x0>0 && x1<0 || x0<0 && x1>0) && (x1>x0 && x0 >0 || x1<x0 && x0 < 0) x0 == 0 1 0 && x1 == 0 1 1 && !(x0>0 && x1<0 || x0<0 && x1>0) && !(x1>x0 && x0>0 || x1<x0 && x0<0) x1' = 0 x0' = 1 1 5


Слайд 18

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);


Слайд 19

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


Слайд 20

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


Слайд 21

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


Слайд 22

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


×

HTML:





Ссылка: