Перспективы интеграции методов верификации программного обеспечения

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

Аннотация. В статье предлагается подход к построению расширяемой среды верификации программных систем, которая, по мнению автора, поможет решить проблемы практической применимости современных строгих методов верификации к практически значимым программам, сложность которых все время растет. Она же может стать аналогом испытательного стенда для апробации и отладки большого числа новых предлагаемых техник формальных верификации и статического анализа на разнообразном промышленном программном обеспечении.

Содержание

1. Введение

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

3. Подход к построению расширяемой среды верификации ПО

3.1. Анализ требований

3.2. Поддержка различных языков и нотаций

3.3. Архитектурная основа среды верификации

3.4. Организация разработки среды верификации

4. Заключение

Литература

1. Введение

Прогресс технологий разработки программного обеспечения (ПО) в последние десятилетия значительно увеличил производительность программистов в терминах количества кода, создаваемого ими в единицу времени. Это проявляется, в частности, в увеличении размеров наиболее сложных программных систем, разрабатываемых сейчас, до десятков миллионов строк кода [1, 2]. Однако качество программ при этом заметным образом не изменилось — среднее количество ошибок на тысячу строк кода, еще не прошедшего тестирование, по-прежнему колеблется в пределах 10-50 [3]. Таким образом, совершенствование методов разработки ПО, давая возможность создавать все более сложные системы, необходимые современной экономике, науке и государственным организациям, парадоксальным образом лишь увеличивает количество дефектов в них и связанные с этим риски.

Борьба с дефектами и ошибками в программном обеспечении ведется при помощи его верификации. В ходе ее выполнения проверяется взаимная согласованность всех артефактов разработки — проектной и пользовательской документации, исходного кода, конфигураций развертывания, — а также их соответствие требованиям к данной системе и нормам применимых к ней стандартов. Методы верификации ПО также активно развиваются, однако их прогресс менее заметен. Поэтому предельная сложность ПО, которое можно сделать надежно и корректно работающим, существенно меньше сложности систем, востребованных современным обществом.

Различные методы проведения верификации ПО можно (больше по историческим, чем содержательным причинам) разделить [4] на формальные методы, использующие строгий анализ математических моделей проверяемых артефактов и требуемых свойств; методы статического анализа, в ходе которых возможные ошибки ищутся без исполнения проверяемого ПО; методы динамического анализа, проводящие проверку реального поведения проверяемой системы в рамках некоторых сценариев ее работы; и экспертизу (review, inspection), выполняемую людьми на основе их знаний и опыта.

Все эти методы имеют разные достоинства и недостатки, различные области применимости, и эффективность их применения сильно отличается в разных контекстах. Но полноценная верификация крупномасштабных сложных систем невозможна без совместного использования всех этих методов, поскольку только их сочетание позволяет преодолеть недостатки каждого. При этом на каждом уровне рассмотрения системы и для каждого вида компонентов хотелось бы выбирать самый эффективный метод, дающий наиболее достоверный вклад в оценку качества системы в целом и требующий минимальных затрат. К сожалению, пока не существует общего подхода, позволяющего сопоставлять и сравнивать различные методы верификации и их сочетания в различных контекстах при применении к реальным программным системам.

Чтобы справиться со все возрастающей сложностью реальных систем, исследователями за последние 20-30 лет создано огромное количество разнообразных методов и техник верификации [4], особенно в рамках статического анализа и формальных методов. Но для их эффективного использования чаще всего нужно быть специалистом в соответствующей области. Многие из таких работ ограничиваются формулировкой идей и алгоритмов, несколько реже создаются прототипные реализации, цель которых — на двух-трех примерах продемонстрировать, что предложенная техника работает. Эти прототипы невозможно использовать для индустриальной разработки ПО, в рамках которой инструменты должны быть работоспособны и эффективны в очень широком контексте. У исследователей же почти никогда нет ресурсов и времени разрабатывать промышленно применимые инструменты.

В тех очень редких случаях, когда удается все же сделать пригодный к использованию на практике инструмент, он объединяет десяток-два разнообразных техник и способен решать две-три задачи верификации. Однако в процессе промышленной разработки ПО таких задач несколько десятков, а большинству организаций удается успешно внедрить и начать активно использовать лишь два-три таких инструмента.

Другой проблемой является растущая сложность создания и апробации новых техник верификации. Все необходимое для их работы окружение — инструменты анализа исходного кода, описания формальных моделей, библиотеки для работы с внутренним представлением моделей и кода, инструменты, реализующие различные виды анализа кода и моделей, средства получения отчетов — невозможно разработать заново. Исследователю для проверки работоспособности его идеи приходится на скорую руку собирать это окружение из разнородных компонентов и библиотек, которые можно найти в свободном доступе. В лучшем случае удается создать прототип, который способен справиться с парой нужных примеров. Но таким способом невозможно создать среду, в рамках которой можно было бы проанализировать работоспособность и эффективность новой идеи в широком множестве разнообразных ситуаций, на разных видах приложений и требований к ним. Поэтому большинство новых идей применяются лишь в «тепличных условиях», а эффекты от их применения в широком контексте остаются неясными и непредсказуемыми.

Решением для упомянутых проблем могла бы стать унифицированная расширяемая среда верификации программных систем, предоставляющая общее окружение для решения задач верификации и библиотеки готовых компонентов, реализующих типовые техники. Такая среда могла бы существенно упростить интеграцию модулей, реализующих различные техники верификации, за счет унифицированных интерфейсов ее расширения.

Исследователи могли бы использовать ее для значительного снижения затрат на апробацию новых методов и анализ их работоспособности в разнообразных ситуациях. Промышленные разработчики — для интеграции нужного им набора техник в рамках единого инструмента и эффективного внедрения их в практическое использование.

Подтверждением работоспособности и эффективности интеграции различных методов верификации ПО в разнообразных ситуациях являются многочисленные синтетические методы верификации.

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

Синтетические методы верификации используют техники различных видов по приведенной выше классификации, а также комбинируют идеи различных подходов для получения большей эффективности верификации в терминах затрат на ее проведение и достоверности получаемых результатов.

На данный момент такие методы относятся к одной из следующих групп.

• Статический анализ предполагает построение некоторых моделей кода проверяемой системы, чаще всего, в виде размеченных графов потоков управления и данных, и анализ свойств этих моделей, например, поиск ошибок определенного рода по соответствующим им шаблонам в потоках данных. Сейчас все чаще используются специфические виды статического анализа, в рамках которых находят применения формальные модели и специализированные инструменты разрешения ограничений.

  • Расширенный статический анализ (extended static checking) [5, 6] проверяет соответствие кода ПО требованиям, обычно записываемым тоже в коде в виде комментариев к его отдельным элементам (процедурам, типам данных и методам классов). При этом на основе результатов анализа кода автоматически строятся формальные модели его поведения, выполнение требований для которых проверяется чаще всего с помощью дедуктивного анализа и специализированных решателей (solvers).
  • Статический анализ на базе автоматической абстракции [7-10]. В рамках такого подхода на основе результатов статического анализа кода автоматически строятся более абстрактные, а потому более простые модели работы проверяемого ПО, которые затем подвергаются проверке на выполнение определенных свойств с помощью инструментов проверки моделей или решателей. Обычно проверяемые свойства фиксированы для данного инструмента или формулируются в конфигурационном файле. При нарушении требования в модели инструменты этого типа пытаются построить соответствующий сценарий работы кода. Если это не получается из-за упрощений, сделанных при построении модели, определяются элементы кода, препятствующие выполнению такого сценария, и в модель вносятся уточнения, более аккуратно описывающие работу именно этих элементов, после уточненная модель снова проверяется на выполнение заданного свойства. В итоге инструмент либо подтверждает выполнение требований, либо находит контрпример, либо завершает работу по истечении некоторого времени или из-за исчерпания ресурсов, не приходя к определенным выводам.

• Синтетическое структурное тестирование [11-16] при котором после первого случайно выбранного теста остальные тесты генерируются автоматически так, чтобы обеспечить покрытие еще не покрытых ранее элементов кода. Для выбора подходящих тестовых данных используются решатели, учитывающие символическую информацию о ранее выполненных тестах (ограничения на данные, отделяющие прошедшие тесты от еще не покрытого кода), а для построения нужных последовательностей воздействий — случайная генерация, направляемая как этой же символической информацией, так и некоторыми эвристическими абстракциями, уменьшающими пространство состояний проверяемой системы.Тестирование на основе моделей (model based testing) [17-19] сочетает разработку формальных моделей требований к проверяемому ПО и построение тестов на базе этих моделей. Структура модели при этом служит основой для критерия полноты тестирования, а ограничения модели на корректные результаты работы ПО используются в качестве тестовых оракулов, оценивающих правильность поведения ПО в ходе тестирования.
  В рамках последних двух подходов (или отдельно от них) применяются специфические техники построения тестов, сами по себе сочетающие разные методы верификации.

  • Построение тестов с помощью разрешения ограничений [20-22]. Часто при разработке тестов на основе критериев полноты тестирования формулируются так называемые цели тестирования (test objectives), представляющие собой специфические ситуации, в которых необходимо проверить поведение тестируемой системы для достижения необходимой уверенности в ее корректной работе. Цель тестирования формулируется как набор ограничений на проходимые во время теста состояния системы и данные выполняемых воздействий. Для построения теста, достигающего такую цель, можно использовать специализированные решатели (solvers). Такой решатель либо автоматически находит необходимые данные и последовательность вызовов операций как решение заданной системы ограничений, либо показывает, что эта система неразрешима, т.е. заданная цель тестирования недостижима и строить нацеленные на нее тесты не имеет смысла.
  • Построение тестов как контрпримеров с помощью инструментов проверки моделей [23-26]. Другой способ построения тестов — сформулировать отрицание ограничений, задающих цель тестирования, как свойство, которое можно проверить или опровергнуть с помощью инструмента проверки моделей. Если это свойство подтверждается, значит, цель тестирования недостижима, если же оно опровергается, то инструмент строит контрпример, являющийся в данном случае необходимым тестом.
• Мониторинг формальных свойств (runtime verification, passive testing) [27-30] тоже использует формальные модели требований для оценки правильности поведения проверяемой системы, но только в ходе ее обычной работы, без использования специально построенных тестов.

Как видно, все синтетические методы так или иначе пытаются соединить достоинства различных подходов к верификации, купируя их недостатки. В настоящее время достигнуты значительные успехи в разработке таких методов и внедрении их в практику промышленной разработки ПО, например, в следующих случаях.

• Многочисленные проекты NASA по разработке ПО управления для космических спутников, челноков и специализированных исследовательских аппаратов, проводимые с использованием инструментов проверки моделей, генерации тестов на их основе и мониторинга [31-33]. Из используемых в этих проектах инструментах наиболее известны инструменты проверки моделей Spin [34, 35], генератор тестов T-VEC [36, 37] и инструмент символического выполнения Java PathFinder [38, 39], используемый для проверки свойств Java программ, их мониторинга и тестирования.
• Создание и использование в Microsoft инструмента Static Driver Verifier, использующего статический анализ с автоматической абстракций для проверки корректности работы драйверов Windows [40]. Сначала в проекте использовался инструмент проверки моделей SLAM, который затем был значительно доработан и дополнен возможностями анализа произвольного кода на языке C и автоматической абстракции, направляемой контрпримерами [41, 42].
• Внутренний проект Microsoft по проведению формальной спецификации и генерации тестовых наборов для разнообразных клиент-серверных протоколов, используемых в продуктах этой компании [43]. В рамках этого проекта используется, в основном, инструмент SpecExplorer [44], разработанный в Microsoft Research, а объем работ по анализу и формализации документации на протоколы оценивается в несколько десятков человеко-лет.
• Проводившиеся и идущие в настоящее время в ИСП РАН проекты по созданию тестов на основе формальных моделей базовых библиотек операционных систем, телекоммуникационных протоколов семейства IPv6, оптимизирующих блоков компиляторов [45-47], использующие семейство инструментов тестирования на основе моделей UniTESK [48].
• Использование формальных методов верификации и инструментов расширенного статического анализа при создании систем авионики в Airbus и Boeing [10, 49, 50]. В частности, в Airbus использовался инструмент статического анализа на основе формальных моделей ASTREE [10].
• Использование формальных методов, тестирования на основе моделей и средств мониторинга при разработке ПО для смарт-карт [51, 52].

Все эти примеры подтверждают эффективность интеграции различных вери-фикационных методов на практике. Тем не менее, несмотря на достигнутые успехи, каждый из имеющихся синтетических подходов использует лишь часть имеющегося потенциала и не предоставляет единой среды интеграции для всего многообразия различных техник верификации ПО.

Содержание Вперёд