Использование формальных методов для обеспечения соблюдения программных стандартов

А. И. Гриневич, В. В. Кулямин, Д. А. Марковцев, А. К. Петренко, В. В. Рубанов, А. В. Хорошилов
Труды Института системного программирования РАН

14.11.2006

Страницы: предыдущая :: 1 :: 2 :: 3 :: 4 :: 5 :: ... :: 7 :: следующая

В основе процесса разработки тестов на соответствие стандарту лежит технология UniTesK, разработанная в ИСП РАН на базе многолетнего опыта проектов по тестированию сложного промышленного ПО. Эта технология использует подход к формальному тестированию, разработанный в работах Берно (Bernot) [7], Бринксмы (Brinksma) и Тритманса (Tretmans) [8,9] и описанный в телекоммуникационных стандартах ISO 9646 [3] и ITU-T Z.500 [4]. Основные положения этого подхода можно сформулировать следующим образом (Рис. 2 иллюстрирует связи между упоминаемыми ниже понятиями).

• Требования стандарта представлены в виде модели, описанной с помощью некоторого формализма. Эта модель называется спецификацией.

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

• Тот факт, что тестовая система соответствует стандарту, моделируется посредством отношения соответствия (conformance relation, implementation relation) между реализацией и спецификацией.

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

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

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

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

Тестовый набор называется полным относительно критерия покрытия, если объединение классов эквивалентности по этому критерию тестов из этого набора есть полный тестовый набор в определенном выше смысле.

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

Технология UniTesK детально рассматривалась в работах [10-13]. Здесь мы приводим только краткое описание ее основных идей.

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

• Критерии тестового покрытия определяются на основе структуры постусловий операций отдельного компонента или нескольких компонентов. Примерами таких критериев являются покрытие ветвей в коде постусловия и покрытие дизъюнктов из дизъюнктивной нормальной формы условий этих же ветвлений. Есть возможность вводить произвольные критерии, описывая дополнительные ситуации, в которых работу системы необходимо проверить.
• Тестовый сценарий создается для достижения определённого покрытия заданной группы операций. Такой сценарий определяет конечный автомат, моделирующий поведение тестируемого компонента таким образом, что выполнение всех его переходов гарантирует покрытие 100% ситуаций в соответствии с выбранным критерием. Автомат задается при помощи функции вычисления состояния и набора допустимых действий в произвольном состоянии. Этот набор действий зависит от данных состояния. Каждое действие соответствует вызову одной из операций с некоторыми аргументами.

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

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

Страницы: предыдущая :: 1 :: 2 :: 3 :: 4 :: 5 :: ... :: 7 :: следующая