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

Таблица 3. Характеристики некоторых методов анализа архитектуры ПО. 
Метод 
Техника 
оценки 
Оцениваемые 
характерис-
тики 
Доп. 
результаты 
Используемые 
описания 
архитектуры 
Возможности 
многократного 
использования 
информации 
SAAM [94] 
Сценарии 
Модифицируе-
мость, 
соответствие 
требованиям
Проблемные 
места 
Статическое 
представление 
— 
ATAM [96] 
Сценарии, 
метрики, спец. 
техники для 
каждого 
атрибута 
качества 
Любые, для 
оценки каждой 
характеристики 
привлекаются 
эксперты 
Точки увязки 
— элементы 
архитектуры, 
влияющие на 
несколько 
характерис-
тик 
Статические и 
динамические 
представления 
Техники 
анализа 
отдельных 
атрибутов 
качества 
SBAR [98] 
Сценарии, мат. 
модели, 
симуляция 
Любые 
— 
Детальные 
представления 
всех проектных 
решений 
— 
ALMA [99] 
Сценарии 
Модифицируе-
мость 
Последствия 
изменений, 
оценка затрат 
на поддержку 
— 
— 
CBAM [100] 
Сценарии, 
сравнительные 
оценки, спец. 
техники для 
каждого 
атрибута 
Любые 
Явные оценки 
выгод и 
стоимости 
проектных 
решений 
Статические и 
динамические 
представления 
Техники 
анализа 
отдельных 
атрибутов 
качества 

---

46 
3.2. 
Статический анализ 
Методы статического анализа артефактов жизненного цикла можно разделить на 
два вида: контроль того, что все формализованные правила корректности построения 
этих артефактов выполнены, и поиск типичных ошибок и дефектов в них на основе 
некоторых шаблонов. Часто инструменты статического анализа используют оба типа 
проверок. 
Чаще всего используется статический анализ исходного кода, см., например, 
список инструментов [102], выполняющих такой анализ, или детальный обзор [103] 
трех из них, PolySpace Verifier [104], Coverity Prevent [105] и Klocwork K7 [106], 
реализующих наиболее сложные виды анализа. Проверенные на практике правила 
корректности кода или шаблоны типичных ошибок переносятся в среды разработки, 
такие как Eclipse или Microsoft Visual Studio, и постепенно становятся семантическими 
правилами языков программирования, их проверка возлагается уже на компиляторы 
этих языков. Поэтому статический анализ можно считать наиболее широко 
применяемым методом верификации.
Если в проекте используются языки описания архитектуры или графические 
языки проектирования, построенные с их помощью артефакты можно также проверять 
с помощью специализированных инструментов, например [107], которые также 
постепенно встраиваются в широко используемые среды моделирования, такие как 
Rational Rose. 
Поэтому методы верификации при помощи статического анализа либо уже 
прошли апробацию на практике и используются в коммерческих инструментах и 
широко применяемых инструментах разработки общего назначения, либо все еще 
остаются в ранге новаторских, исследовательских работ. Исследовательские методы на 
данный момент, в основном, связаны с формализацией различных характеристик и 
свойств ПО и поэтому рассматриваются в разделе, посвященным синтетическим 
подходам к верификации. 

---

47