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

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

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

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

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

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

Сложность задач и интерфейса
/ 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 = x1-x0; x1 = x1-x0; x0 = x0+x1; }
x1 = x0-x1;
x0 = x0-x1;
}
return x0;
}
/ 23

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

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

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

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

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

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

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

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

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

Пример работы DART
/ 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 = 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 == 0
1
0
&& x1 == 0
1
1
&& !(x0>0 && x1<0 || x0<0 && x1>0)
&& !(x1>x0 && x0>0 || x1
x1' = 0
x0' = 1
1
5

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

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

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

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