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

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

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

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

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

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

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

Никакая верификация немыслима без предварительной четкой формулировки проверяемых требований, и на практике почти всегда любая деятельность по верификации предваряется анализом требований к проверяемой системе и (обычно, частичной) их формализацией.

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

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

Еще один важный аспект — место экспертизы среди поддерживаемых рассматриваемой средой подходов к верификации. Экспертиза применима к любым свойствам ПО и любым артефактам, хотя для разных целей используются разные ее виды. Она позволяет выявлять все виды ошибок, причем делать это на ранних этапах, тем самым минимизируя время существования дефекта в рамках жизненного цикла ПО и ресурсы, требующиеся на его устранение. Эмпирические исследования показывают, что эффективность экспертиз, измеряемая как отношение количества обнаруживаемых дефектов к затрачиваемым на это ресурсам, выше, чем для других методов верификации. Согласно различным отчетам от 50% до 90% всех зафиксированных в жизненном цикле ПО ошибок может быть обнаружено с помощью экспертиз [54-56].

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

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

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

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

Опыт, полученный на основе большого числа проектов по верификации промышленного ПО [18, 19, 43, 44, 46, 48], позволяет утверждать, что использование в рамках технологий и инструментов языков, которые как можно меньше отличаются от привычных обычным разработчикам, существенно облегчает их внедрение и использование в промышленности. Поэтому в рамках среды в первую очередь необходимо использовать такие формы представления моделей, которые были бы минимально необходимыми расширениями широко распространенных языков программирования. В дальнейшем можно добавлять поддержку для наиболее известных языков формальных спецификаций.

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

При наличии такой возможности стоит использовать уже имеющиеся стандартные или широко используемые библиотеки для работы с промежуточным представлением для ряда языков. Например, для C и C++ стандартом де-факто постепенно становится промежуточное представление, используемое в рамках компилятора GCC [57]. Значительным преимуществом использования результатов подобных проектов является гарантированные их поддержка и развитие в будущем в течение обозримого времени.

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

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

Прежде всего, для облегчения ее использования в промышленной разработке ПО, такая среда должна быть встроена в одну из широко используемых сред разработки, таких как Eclipse или Microsoft Visual Studio. Eclipse [58, 59] является наиболее подходящей средой интеграции для первых версий, поскольку обладает огромным набором модулей расширения, в том числе являющихся инструментами верификации и модулями поддержки различных языков программирования. Кроме того, процессом создания таких модулей хорошо документирован.

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

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

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

Чтобы в архитектурный каркас тестирования на основе моделей вложить другие синтетические методы верификации, необходимо лишь добавить модули для анализа исходного кода проверяемых компонентов — все остальные необходимые модули в нем фактически уже имеются (см. также [60]).

Рис. 1. Предварительная архитектура расширяемой среды верификации ПО.

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

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

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

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

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

Для начала такого проекта важно подготовить общий каркас среды и реализацию некоторой значимой части ее функциональности. В качестве первого варианта можно рассматривать расширение системы модульного тестирования TestNG [61, 62] с помощью средств построения тестов на основе моделей. TestNG — это популярная среда c открытым кодом, поддерживающая разработку модульных и интеграционных тестов для Java приложений и позволяющая гибко конфигурировать выполнение полученных тестовых наборов. Расширение ее возможностями тестирования на основе моделей и хотя бы одним-двумя видами анализа моделей и кода, позволяющими, например, реализовать синтетическое структурное тестирование в ряде ситуаций, позволит наглядно продемонстрировать интеграционные возможности предлагаемого подхода.

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

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

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

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

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

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