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

       

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


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

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

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

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

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


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



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

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

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


Содержание раздела