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

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

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

/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)]

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

/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

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

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

/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

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

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

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

/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

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

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

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