Синтетические методы верификации

Лекция 7: Синтетические методы верификации. Тестирование на основе моделей и мониторинг формальных свойств программного обеспечения. Методы статического анализ формальных свойств и синтетические методы генерации структурных тестов Синтетические методы верификации сочетают техники нескольких типов – статический анализ, формальный анализ свойств ПО, тестирование. Некоторые из таких методов породили самостоятельные бурно развивающиеся области исследований, в первую очередь, тестирование на основе моделей и мониторинг формальных свойств (runtime verification, passive testing). Тестирование на основе моделей Тестирование на основе моделей (model based testing) использует для построения тестов формальные модели требований к ПО и принятых проектных решений. Как критерии полноты тестирования, так и оракулы строятся на основе информации, содержащейся в этих моделях. Получаемые в результате тесты обычно слабо связаны со специфическими особенностями программной реализации тестируемой системы, но содержат представительный набор ситуаций с точки зрения исходной модели. Истоки методологии тестирования на основе моделей лежат в проведенных в 1950-х годах исследованиях возможности определения структуры конечного автомата, моделирующего поведение данной системы, на основе результатов экспериментов с этой системой. Впоследствии были разработаны методы, позволяющие на основе модели в виде конечного автомата строить наборы тестов, успешное выполнение которых при определенных ограничениях на проверяемую систему гарантирует эквивалентность поведения этой системы заданной модели. В конце 1980-х годов интерес к тестированию на основе моделей возобновляется, и начинают разрабатываться новые подходы, использующие другие виды моделей, помимо конечных автоматов. Основной области их применения в то время было тестирование реализаций телекоммуникационных протоколов на соответствие стандартам этих протоколов. Примерно в это время разрабатывается стандарт ISO 9646 на такое тестирование, учитывающий возможность использования формальных моделей. С середины 1990-х годов тестирование на основе моделей начинает использоваться для других видов программных систем за счет использования более хорошо масштабируемых моделей в виде программных контрактов. В настоящее время методы тестирования на основе моделей используют следующие типы моделей и техник. Методы проверки согласованности автоматов и систем переходов. Такие методы относятся к одному из трех типов, в зависимости от используемых моделей. Обычные и расширенные конечные автоматы. Методы построения тестов на основе конечных автоматов наиболее глубоко разработаны, известны их точные ограничения и гарантии полноты выполняемых проверок. Методы, использующие расширенные автоматы, сводят их к обычным, но применяют более детальные критерии покрытия, основанные на использовании данных в расширенных автоматах. Наиболее известными инструментами создания тестов на основе таких моделей являются BZ-TT, использующий модели, описанные на языке B, и Gotcha-TCBeans, использующий язык Mur ϕ или UML Statecharts в рамках набора инструментов AGEDIS. Системы переходов. Такие методы чаще используются при тестировании распределенных систем, поскольку моделирование таких систем с помощью конечных автоматов очень трудоемко. Большинство этих методов не определяют практически применимых критериев полноты и не дают конечных тестовых наборов для реальных систем, поэтому использующие их инструменты опираются на те или иные эвристики для обеспечения конечности набора тестов. Первые методы построения тестов по LTS-моделям были разработаны в работах Бринксмы и Тритманса. Наиболее известны из инструментов, созданных на основе результатов Тритманса, TorX и TGV. Последний инструмент входит в набор инструментов верификации CADP. Помимо обычных систем переходов используются и временные (расширенные с помощью таймеров), построение тестов на их основе возможно с использованием инструмента UPAAL. Программные контракты. В методах такого рода описание требований к тестируемой системе представляет собой набор программных контрактов, иногда с дополнительным определением явного преобразования состояния системы. Тесты строятся на основе автоматных моделей, являющихся абстракциями от этих контрактов. Примеры инструментальной поддержки таких методов — инструменты технологии UniTESK, созданной в ИСП РАН, и инструмент SpecExplorer, разработанный в Microsoft Research. Методы построения тестов на основе формального анализа свойств ПО используют формальный анализ для классификации тестовых ситуаций и нацеленной генерации тестов. Методы на основе проверки моделей. В рамках таких методов тестовые ситуации выбираются как представители классов эквивалентности, задаваемых критерием покрытия. Соответствующая ситуации тестовая последовательность строится как контрпример при проверке модели (model checking) на выполнение свойства, являющегося отрицанием условия достижения этой ситуации. Методы на основе дедуктивного анализа. В этих методах выбираемые тестовые ситуации соответствуют особым случаям в дедуктивном анализе свойств тестируемой системы. Методы построения тестов с помощью символического выполнения (symbolic execution). Такие методы используют символическое описание проходимого во время выполнения теста пути по тексту программы (или формальных проверяемых спецификаций) в виде набора предикатов. Это описание позволяет выбирать новые тестовые ситуации так, чтобы они покрывали другие пути и строить тесты с помощью техник разрешения ограничений (constraint solving). Символическое выполнение в комбинации с конкретизацией тестовых данных используется и для построения тестов, нацеленных на типичные дефекты, такие, как использование неинициализированных объектов, тупики и гонки параллельных потоков. Можно отметить, что наиболее развиты методы тестирования на основе моделей первой из перечисленных выше групп. Поддерживающие их инструменты все шире начинают использоваться в промышленных проектах. Методы построения тестов на основе проверки моделей и на основе символического выполнения активно развиваются и начинают воплощаться в инструменты. Мониторинг формальных свойств ПО Мониторинг формальных свойств ПО (для этой области используется два английских термина — runtime verification и passive testing) стал развиваться как отдельное направление исследований в конце 1990-х годов. В основе этого подхода лежит фиксация формальных свойств ПО, которые необходимо проверить и встраивание их проверок в систему мониторинга. В дальнейшем выполняется мониторинг ПО, в ходе которого контролируются и выделенные свойства. В публикациях упоминаются следующие методы мониторинга формальных свойств ПО. Использующие описание свойств с помощью обычных и временных логик. Подобные техники осуществляют контроль свойств, записанных в виде формул временных логик, с помощью записи событий, происходящих в работающем ПО и анализа возникающих трасс. Один из инструментов, использующих такие техники — Temporal Rover. Использующие описание свойств в виде систем переходов или автоматов. В этих техниках трасса анализируется не на выполнение некоторых формул, а на согласованность с заданной автоматной моделью правильного поведения. Использующие программные контракты. В рамках таких подходов корректность поведения системы проверяется во время ее работы с помощью оракулов на базе программных контрактов, внедренных в систему мониторинга. Пока методы мониторинга формальных свойств используются не в исследовательских целях достаточно редко, в основном, для мониторинга небольших критических приложений. Так, NASA применяет несколько таких инструментов, в том числе, разработанный силами собственных сотрудников Java PathExplorer, для верификации систем управления спутниковыми системами. Статический анализ формальных свойств Методы статического анализа формальных свойств исследуются уже несколько десятилетий, но только в самом конце XX – начале XXI века появились реализующие их инструменты, пригодные для применения к сложным программным системам. По используемым этими инструментами техникам формального анализа их можно разделить на следующие группы. Методы на основе генерации верификационных утверждений (verification conditions) и их дедуктивного анализа. Подобные методы статического анализа были названы расширенным статическим анализом (extended static checking). На них основаны такие инструменты как ESC/Java 2 ] или Boogie, требующие пополнения кода ПО предусловиями и постусловиями отдельных функций (часто также инвариантами типов данных и циклов), и не требующие вмешательства человека инструменты, такие как Saturn или Calysto, нацеленные на поиск типичных ошибок. Методы на основе проверки свойств моделей, автоматически создаваемых на основе исходного кода. Такие методы используют так называемую абстрактную интерпретацию (abstract interpretation) для построения простых моделей поведения кода, которые позволяют проверить определенные свойства, но могут терять информацию, касающуюся других свойств. Такие методы, в свою очередь, делятся на две группы. Методы на основе булевских моделей. Эти модели являются конечными наборами булевских значений, выбираемыми так, чтобы достаточно точно можно было анализировать возможные сценарии выполнения программы. Такие модели используются в инструменте Blast и в SLAM, который был переработан в Microsoft в Static Driver Verifier, используемый для эффективного поиска ошибок, связанных с использованием ресурсов операционной системы в драйверах Microsoft Windows. Методы на основе разнородных моделей. Такие техники используют более сложные модели, чем булевские (например, представление областей возможных значений переменных в виде выпуклых многогранников или деревья выбора значений числовых переменных в зависимости от набора булевских), которые позволяют эффективнее анализировать специфические свойства ПО. К инструментам такого рода относятся ASTREE и PolySpace Verifier. Хотя инструменты статического анализа формальных свойств появились не так давно, некоторые из них (SLAM в виде Static Driver Verifier) уже используются в промышленном программировании. Стоит обратить внимание, что при практическом использовании основным недостатком инструментов статического анализа становится большое количество сообщений о возможных ошибках или дефектах, которые таковыми не являются. При работе с программными системами размеров в несколько сотен тысяч строк могут возникать тысячи таких сообщений, проанализировать их вручную в этих случаях не представляется возможным. Поэтому большое количество исследований ведется в направлении создания инструментов, выдающих как можно меньше ложных сообщений об ошибках, и в то же время, не пропускающих серьезные дефекты. Синтетические методы генерации структурных тестов В последние 25 лет активно разрабатываются инструменты автоматической генерации тестов на основе текстов программ, которые используют дополнительные источники информации. В качестве таких источников выступают статический анализ текстов программ, формальный анализ, мониторинг выполнения ранее построенных тестов и т.п. Поскольку в инструментах этого типа используется обычно 3-4 техники разных типов по используемой ранее классификации, методы, лежащие в их основе, вынесены в отдельную разновидность синтетических методов верификации. Характерным для этих инструментов примером является развитие инструмента JCrasher, созданного в 2003-2004 годах в университете Орегона, впоследствии переработанного сначала в Check-n-Crash, а затем – в DSDCrasher. JCrasher генерирует структурные тесты для Java-программ, используя случайные данные примитивных типов, несколько простых эвристик нацеливания на вероятные ошибки, синтаксис операций и структуру данных. Получаемый тест представляет собой последовательность вызовов операций, аргументы которых могут быть сгенерированы случайно или получены как результаты предыдущих вызовов. Выполняемые проверки сводятся к отсутствию исключений и сбоев. В инструменте статического анализа Check-n-Crash реализации добавлен тестируемых предварительный операций, на этап котором выделяются предикаты, соответствующие различным путям выполнения операций, которые затем разрешаются частично с помощью разрешения ограничений, частично за счет небольших модификаций случайных тестов. DSDCrasher добавляет еще одну предварительную фазу, на которой тестируемая программа выполняется на множестве случайных сценариев, и с помощью дополнительного инструмента Daikon выявляются ее возможные инварианты и ограничения. Затем они используются для отсеивания некорректных сценариев тестирования, которые приводят к ошибкам не в силу ошибочной работы программы, а из-за неправильного ее использования. Другие примеры подобной интеграции различных техник верификации в инструментах генерации структурных тестов дают инструменты Randoop и SMART. Они также основаны на случайной генерации последовательностей тестовых вызовов, нацеливаемой на сложные ошибки взаимодействия. В Randoop это нацеливание происходит за счет сокращения множества возможных состояний тестируемой программы при помощи символического анализа выполнения получаемых тестов и использования эвристик попадания в новые ситуации – иногда генерируются длинные последовательности одинаковых вызовов. SMART вместе с символическим выполнением использует выделение возможных ограничений, как и DSDCrasher.