ПРОГРАММИРОВАНИЕ, 2009, № 4, с. 41-55
■ ТЕСТИРОВАНИЕ, ВЕРИФИКАЦИЯ И ВАЛИДАЦИЯ ПРОГРАММ
УДК 004.92+004.94
ИНТЕГРАЦИЯ МЕТОДОВ ВЕРИФИКАЦИИ ПРОГРАММНЫХ СИСТЕМ
© 2009 г. В. В. Кулямин
Институт системного программирования РАН 109004 Москва, ул. Солженицына, 25 E-mail: kuliamin@ispras.ru Поступила в редакцию 24.12.2008 г.
В статье предлагается подход к построению расширяемой среды верификации программных систем, которая, по мнению автора, поможет решить проблемы практической применимости современных строгих методов верификации к практически значимым программам, сложность которых все время растет. Она же может стать своего рода испытательным стендом для апробации и отладки большого числа новых предлагаемых техник формальной верификации и статического анализа на разнообразном промышленном программном обеспечении.
1. ВВЕДЕНИЕ
В последние 20 лет мы являемся свидетелями значительного прогресса технологий разработки программного обеспечения (ПО). Этот прогресс, в частности, существенно увеличил производительность программистов в терминах количества кода, создаваемого ими в единицу времени, что проявляется в увеличении размеров наиболее сложных программных систем, разрабатываемых сейчас, до десятков миллионов строк кода [1, 2]. Однако качество программ при этом заметным образом не изменилось - среднее количество ошибок на тысячу строк кода, еще не прошедшего тестирование, по-прежнему колеблется в пределах 10-50 [3]. Таким образом, совершенствование методов разработки ПО, давая возможность создавать все более сложные системы, необходимые современной экономике, науке и государственным организациям, парадоксальным образом лишь увеличивает количество дефектов в них и связанные с этим риски.
Борьба с дефектами и ошибками в программном обеспечении ведется при помощи его верификации. В ходе ее выполнения проверяется взаимная согласованность всех артефактов разработки - проектной и пользовательской документации, исходного кода, конфигураций развертывания, - а также их соответствие требова-
ниям к данной системе и нормам применимых к ней стандартов. Методы верификации ПО также активно развиваются, однако их прогресс менее заметен, чем развитие технологий разработки. Поэтому предельная сложность ПО, которое можно сделать надежно и корректно работающим, существенно меньше сложности систем, востребованных современным обществом.
Различные методы проведения верификации ПО можно (больше по историческим, чем содержательным причинам) разделить [4] на формальные методы, использующие строгий анализ математических моделей проверяемых артефактов и требуемых свойств; методы статического анализа, в ходе которых возможные ошибки ищутся без исполнения проверяемого ПО; методы динамического анализа, проводящие проверку реального поведения проверяемой системы в рамках некоторых сценариев ее работы; и экспертизу (review, inspection), выполняемую людьми на основе их знаний и опыта.
Все эти методы имеют разные достоинства и недостатки, различные области применимости, и эффективность их применения сильно отличается в разных контекстах. Но полноценная верификация крупномасштабных сложных систем невозможна без совместного использования всех этих методов, поскольку только их сочетание
позволяет преодолеть недостатки каждого. При этом на каждом уровне рассмотрения системы и для каждого вида компонентов хотелось бы выбирать самый эффективный метод, дающий наиболее достоверный вклад в оценку качества системы в целом и требующий минимальных затрат. К сожалению, пока не существует общего подхода, позволяющего сопоставлять и сравнивать эффективность различных методов верификации и их сочетаний в различных контекстах при применении к реальным программным системам.
Чтобы справиться со все возрастающей сложностью реальных систем, исследователями за последние 20-30 лет создано огромное количество разнообразных методов и техник верификации [4], особенно в рамках статического анализа и формальных методов. Но для их эффективного использования чаще всего нужно быть специалистом в соответствующей области. Многие из таких работ ограничиваются формулировкой идей и алгоритмов, несколько реже создаются прототипные реализации, цель которых - на двух-трех примерах продемонстрировать, что предложенная техника работает. Эти прототипы невозможно использовать для индустриальной разработки ПО, в рамках которой инструменты должны быть работоспособны и эффективны в очень широком контексте. У исследователей же почти никогда нет ресурсов и времени разрабатывать промышленно применимые инструменты.
В тех очень редких случаях, когда удается все же сделать пригодный к использованию на практике инструмент, он объединяет десяток-два разнообразных техник и способен решать две-три задачи верификации. Однако в процессе промышленной разработки ПО таких задач -несколько десятков, а большинству организаций удается успешно внедрить и начать активно использовать лишь два-три таких инструмента.
Другой проблемой является растущая сложность создания и апробации новых техник верификации. Все необходимое для их работы окружение - инструменты анализа исходного кода, описания формальных моделей, библиотеки для работы с внутренним представлением моделей и кода, инструменты, реализующие различные виды анализа кода и моделей, средства получения отчетов - невозможно разработать зано-
во. Исследователю для проверки работоспособности его идеи приходится на скорую руку собирать это окружение из разнородных компонентов и библиотек, которые можно найти в свободном доступе. В лучшем случае удается создать прототип, который способен справиться с парой нужных примеров. Но таким способом невозможно создать среду, в рамках которой можно было бы проанализировать работоспособность и эффективность новой идеи в широком множестве разнообразных ситуаций, на разных видах приложений и требований к ним. Поэтому большинство новых идей применяются лишь в "тепличных условиях", а эффекты от их применения в широком контексте остаются неясными и непредсказуемыми.
Решением для упомянутых проблем могла бы стать унифицированная расширяемая среда верификации программных систем, предоставляющая общее окружение для решения задач верификации и библиотеки готовых компонентов, реализующих типовые техники. Такая среда могла бы существенно упростить интеграцию модулей, реализующих различные техники верификации, за счет унифицированных интерфейсов ее расширения.
Исследователи могли бы использовать ее для значительного снижения затрат на апробацию новых методов и анализ их работоспособности в разнообразных ситуациях. Промышленные разработчики - для интеграции нужного им набора техник в рамках единого инструмента и эффективного внедрения их в практическое использование.
Подтверждением работоспособности и эффективности интеграции различных методов верификации ПО в разнообразных ситуациях являются многочисленные синтетические методы верификации.
2. СИНТЕТИЧЕСКИЕ МЕТОДЫ ВЕРИФИКАЦИИ ПО
Синтетические методы верификации используют техники различных видов по приведенной выше классификации, а также комбинируют идеи различных подходов для получения большей эффективности верификации в терминах затрат на ее проведение и достоверности получаемых результатов.
На данный момент такие методы относятся к одной из следующих групп.
• Статический анализ предполагает автоматическое построение некоторых моделей кода проверяемой системы и проверку корректности этих моделей относительно некоторого набора правил (например, перед каждым использованием переменная должна быть инициализирована), а также поиск определенных видов ошибок по соответствующим им шаблонам (например, разыменование указателя корректно только после его проверки на неравенство нулю). В качестве моделей обычно выступают размеченные графы потоков управления и данных. Сейчас же все чаще используются специфические виды статического анализа, в рамках которых находят применения формальные модели и различные инструменты разрешения ограничений, используемые для более глубокого анализа свойств кода.
о Расширенный статический анализ (extended static checking) [5-10] проверяет соответствие кода ПО требованиям, обычно записываемым тоже в коде, например, в виде комментариев к его отдельным элементам (процедурам, типам данных и методам классов). При этом на основе результатов анализа кода автоматически строятся формальные модели его поведения, выполнение требований для которых проверяется чаще всего с помощью дедуктивного анализа (theorem proving) и решателей (solvers). В рамках этого подхода статический анализ интегрируется с одним из формальных методов верификации - дедуктивным анализом. Примерами такого синтеза служат инструменты ESC/Java2 [6, 7], Boogie [8], Saturn [9], Calysto [10].
о Статический анализ на базе автоматической абстракции [11, 14-19]. При использовании таких методов на основе результатов статического анализа кода автоматически строятся более абстрактные, а потому более простые модели работы проверяемого ПО, кото-
рые затем подвергаются проверке на выполнение определенных свойств с помощью инструментов проверки моделей (model checking) или специализированных решателей. Здесь также интегрируются статический анализ и дедуктивный анализ или проверка моделей. Отличие от предыдущего подхода заключается в том, что проверяемые свойства имеют вид общих правил корректности кода - разыменовывать можно только ненулевые указатели, нельзя обращаться к элементу массива за пределами его размера, на всяком пути после захвата ресурса должно быть его освобождение, и т.п., - а не специфичными для проверяемого компонента требованиями. Соответственно, такие правила фиксированы для данного инструмента. Иногда возможна выборочная проверка правил из некоторого достаточно большого списка.
Примером используемых абстрактных моделей служат булевские модели [11] - наборы флагов, концентрированно представляющих необходимую для анализа свойств программы информацию, например, об условиях ветвлений и циклов. Другой пример -восьмиугольники [12] - наборы ограничений вида х ± у G [а,Ь], где х и у - переменн
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.