Синтетические инструменты структурного тестирования Базовые сведения В. Кулямин. - презентация

1 Синтетические инструменты структурного тестирования Базовые сведения В. Кулямин

2 /16 Методы верификации Экспертиза Формальные методы Дедуктивный анализ (theorem proving) Проверка моделей (model checking) Проверка согласованности (conformance checking) Статический анализ Проверка правил корректности Поиск шаблонов ошибок Динамический анализ Мониторинг Создание тестов

3 /16 Гибридные техники Дедуктивный анализ Статический анализ Мониторинг Символическое выполнение Формальны й мониторинг Извлечение ограничений Проверка моделей Создание тестов Разрешение ограничений Вероятностные структурные тесты Абстрактные модели Расширенный статический анализ

4 /16 Символическое выполнение Symbolic execution 1976 James C. King (IBM) Lori A. Clark (University of Massachusetts) if(x > 0) { y := x+2; } else if(x > -1) { y := x+1; } else { y := x; } [(x > 0) (y = x+2)] & [(x 0 & x > - 1) (y = x+1)] & [[(x - 1) (y = x)]

5 /16 Абстрактные модели (abstract domains) Абстрактная интерпретация1977 Patrick Cousot, Radhia Cousot CNRS Восьмиугольники x y a Полиэдры Наборы объектов (heap structures) Битовые векторы …... while ( (x == 0) && (2*f(x)

6 /16 Расширенный статический анализ ESC/Modula 31998DEC Greg Nelson, K. Rustan M. Leino et al. ESC/Java2000 Compaq Leino, Cormac Flanagan ASTREE2002 Cousot ESC/Java Simplify Spec# Checker2004Microsoft Research Leino Boogie

7 /16 Формальный мониторинг Runtime verification1999 NASA Klaus Havelund, Willem Visser Java Path Finder + символическое выполнение

8 /16 Извлечение ограничений Daikon1999MIT Michael D. Ernst =,,

9 /16 Разрешение ограничений Solvers SMT solvers – Satisfiability modulo Theory CVC2002Stanford David L. Dill, Clarke W. Barrett, Aaron Stump Yices2005SRI International Bruno Dutertre, Leonardo de Moura Z32006Microsoft Research Leonardo de Moura, Nikolaj S. Bjørner

10 /16 Генерация структурных тестов Нацеливание на покрытие путей в коде Оракул – отсутствие исключений NullPointer, IndexOutOfBounds, ClassCast, DivideByZero, IllegalArgument Источники тестовых данных и последовательностей Эвристики Вероятностная генерация Символическое выполнение Подходы «Взлом» Динамически нацеливаемое тестирование Генерация тестов по шаблонам

11 /16 «Взлом» Yannis Smaragdakis, Christoph Csallner JCrasher Check-n-Crash2005 DSD-Crasher2006 Daikon ESC/Java 2 solver

12 /16 Динамически нацеливаемые тесты I Patrice Godefroid, Gul Agha, Koushik Sen DART2005 CUTE2005 Consolic testing (concrete + symbolic) jCUTE2006 Обычное выполнение Программа Символическое выполнение Поиск новых путей

13 /16 Динамически нацеливаемые тесты II SAGE2007 SMART2007 CREST2008http://code.google.com/p/crest/ h: ; h: ; h: ; h: ; h: ; h: ; h: ;.... Generation 0 – initial input – 100 bytes of h: ; RIFF h: ; h: ; h: ; h: ; h: ; h: ;.... Generation h: ** ** ** ; RIFF....*** h: ; h: ; h: ; h: ; h: ; h: ;.... Generation h: D ** ** ** ; RIFF=...*** h: ; h: ; h: ; h: ; h: ; h: ;.... Generation h: D ** ** ** ; RIFF=...*** h: ; h: ; h: ;....strh h: ; h: ; h: ;.... Generation h: D ** ** ** ; RIFF=...*** h: ; h: ; h: ;....strh....vids h: ; h: ; h: ;.... Generation h: D ** ** ** ; RIFF=...*** h: ; h: ; h: ;....strh....vids h: ;....strf h: ; h: ;.... Generation h: D ** ** ** ; RIFF=...*** h: ; h: ; h: ;....strh....vids h: ;....strf....( h: ; h: ;.... Generation h: D ** ** ** ; RIFF=...*** h: ; h: ; h: ;....strh....vids h: ;....strf....( h: C9 9D E4 4E ; ÉäN h: ;.... Generation h: D ** ** ** ; RIFF=...*** h: ; h: ; h: ;....strh....vids h: ;....strf....( h: ; h: ;.... Generation h: D ** ** ** ; RIFF=...*** h: ; h: ; h: ;....strh....vids h: B A ;....strf²uv:( h: ; h: ;.... Generation 10 – bug ID ! Found after only 3 generations starting from well-formed seed file

14 /16 Генерация тестов по шаблонам David Notkin, Tao Xie Wolfram Schulte, Nikolai Tillmann, Jonathan de Halleux Symstra2005 MUTT2006 Pex2008

15 /16 Другие инструменты Eclat2005 EXE2005 Randoop2007 …

16 /16 Конец Спасибо за внимание