Архитектура тестовой системы AVM
Тестовые системы, создаваемые с использованием технологии AVM, должны быть разбиты на несколько слоев (см. Рис. 1). Самый нижний уровень — это RTL-модель тестируемого устройства (DUT, Design Under Test). Над ним находится прослойка транзакторов (transactors) — компонентов тестовой системы, осуществляющих преобразование потока входных транзакций во входные сигналы тестируемой модели и наоборот преобразование выходных сигналов тестируемой модели в поток выходных транзакций.
Примерами транзакторов являются: драйвер (driver) — конвертирует поток транзакций во входные сигналы тестируемой модели; ответчик (responder) — отвечает на запросы со стороны тестируемой модели относительно подачи дополнительных данных; монитор (monitor) — осуществляет наблюдение за выходами тестируемой модели, не оказывая на нее влияния.
Следующим слоем является так называемый слой операций (operational layer). Компоненты этого уровня образуют тестовое окружение необходимое тестируемой модели. К ним относятся: генератор стимулов (stimulus generator) — создает поток входных транзакций (стимулов) на тестируемую модель. Для генерации стимулов используется подход на основе разрешения ограничений с использованием рандомизации (CRV, Constraint-Random Verification). Связь генератора с тестируемой моделью осуществляется через драйвер. главный модуль (master) — элемент окружения тестируемой модели, инициирующий взаимодействие с ней. Главный модуль посылает последовательности транзакций (случайные или направленные на достижение какой-либо ситуации) и может использовать обратную связь для определения своих следующих действий. Связь главного модуля с тестируемой моделью осуществляется через драйвер; подчиненный модуль (slave) — как и главный модуль моделирует окружение тестируемой модели, но, в отличие от него, является пассивным компонентом, отвечающим на запросы тестируемой модели. Связь подчиненного модуля с тестируемой моделью осуществляется через ответчик.
Далее следует слой анализа (analysis layer), компоненты которого проверяют корректность поведения тестируемой модели, оценивают полноту тестирования и выполняют некоторые другие функции.
Основными компонентами этого уровня являются:
компонент проверки (scoreboard) — проверяет корректность поведения тестируемой модели в ответ на входные транзакции. сборщик покрытия (coverage collector) — оценивает полноту тестирования путем подсчета числа событий заданных типов, возникающих в процессе тестирования.
На самом верху находится слой управления, включающий в себя один единственный компонент — контроллер теста (test controller), который осуществляет координацию работы других компонентов тестовой системы. Рис. 1 иллюстрирует многослойную структуру тестовой системы. Каждый прямоугольник соответствует определенному слою. В левой части указано его название, в правой — основные компоненты тестовой системы, образующие данный слой. Стрелки показывают взаимодействие между слоями.
Рисунок 1. Слои тестовой системы AVM
Архитектура тестовой системы OVM
В рамках технологии OVM тестовая система собирается из специальных блоков, называемых OVC (Open Verification Component). Каждый блок инкапсулирует тестовое окружение для отдельного модуля аппаратуры и состоит из полного набора компонентов, обеспечивающих генерацию стимулов, проверку правильности поведения и оценку полноты тестирования. Если тестируемая модель аппаратного обеспечения получается путем интеграции нескольких модулей, тестовая система для нее строится путем объединения соответствующих OVC-блоков и построения над ними специального синхронизирующего контроллера (virtual sequencer).
Структура OVC-блоков практически полностью соответствует архитектуре тестовой системы AVM. Пример блока тестовой системы приведен на Рис. 2.
Рисунок 2. Блок тестовой системы
Архитектура тестовой системы UniTESK
Тестовая система UniTESK состоит из следующих основных компонентов (см. Рис. 3):
Обходчик является библиотечным компонентом тестовой системы. В его основе лежит алгоритм обхода графа состояний конечного автомата, моделирующего целевую систему на некотором уровне абстракции. Итератор тестовых воздействий работает под управлением обходчика и предназначен для перебора в каждом достижимом состоянии конечного автомата допустимых тестовых воздействий. Он автоматически генерируется из тестового сценария, который представляет собой описание конечно-автоматной модели тестируемой системы. Тестовый оракул оценивает правильность поведения тестируемой системы в ответ на единичное тестовое воздействие. Он автоматически генерируется на основе формальных спецификаций, описывающих требования к системе в виде пред- и постусловий интерфейсных операций и инвариантов типов данных. Медиатор связывает формальные спецификации с конкретной реализацией тестируемой системы. Медиатор преобразует единичное тестовое воздействие из спецификационного представления в реализационное, а полученную в ответ реакцию — из реализационного представления в спецификационное. Также медиатор синхронизирует состояние спецификации с состоянием тестируемой системы. Трасса теста отражает события, происходящие в процессе тестирования. На основе трассы можно автоматически генерировать различные отчеты, помогающие в анализе результатов тестирования.
Рисунок 3. Архитектура тестовой системы UniTESK
Помимо основных компонентов в тестовой системе выделяются части, отвечающие за интеграцию с конкретным HDL-языком. Например, для языка Verilog такими компонентами являются VPI-модуль (включая VPI-медиатор) и Verilog-окружение.
Литература
IEEE Standard VHDL Language Reference Manual. IEEE Std 1076-1987. IEEE Standard Hardware Description Language Based on the Verilog Hardware Description Language. IEEE Std 1364-1995. IEEE Standard SystemC Language Reference Manual. IEEE Std 1666-2005. IEEE Standard for SystemVerilog – Unified Hardware Design, Specification, and Verification Language. IEEE Std 1800-2005. Adam Rose, Tom Fitzpatrick, Dave Rich, Harry Foster. . Mentor Graphics Corporation, 2008. . Mentor Graphics Corporation, Cadence, 2007. В.П. Иванников, А.С. Камкин, В.В. Кулямин, А.К. Петренко. . Препринт ИСП РАН, 2005.
Обзор технологии AVM
Технология AVM (от англ. advanced verification methodology — передовая методология верификации) была создана в компании Mentor Graphics и распространяется под лицензией Apache 2.0. На настоящий момент она никак не стандартизирована и вся информация по ней находится в «книге рецептов» и пользовательской инструкции по эксплуатации.
Обзор технологии OVM
Технология OVM (от англ. open verification methodology — открытая методология верификации) является совместной разработкой компаний Mentor Graphics и Cadence Design Systems. OVM представляет собой первый открытый промышленный метод разработки тестов на основе языка SystemVerilog . Предшественниками OVM являются подходы AVM (от Mentor Graphics) и URM (от Cadence Design Systems). Технология OVM пока не стандартизирована, но является главным претендентом на звание стандарта.
Обзор технологии UniTESK
Технология UniTESK (от англ. unified specification and testing tool kit — унифицированный инструментарий для спецификации и тестирования) разработана в Институте системного программирования РАН. В отличие от рассмотренных ранее технологий AVM и OVM, созданных в коммерческих организациях, UniTESK является академической разработкой, которая, тем не менее, основана на реальном опыте тестирования программного и аппаратного обеспечения.
Основные понятия
Под моделями аппаратного обеспечения в данной статье понимаются программные модели цифровых устройств, описанные на специальных языках. Такие языки можно разбить на две разновидности: языки описания аппаратуры (HDLs, Hardware Description Languages), с помощью которых разрабатывается модель уровня регистровых передач (RTL, Register Transfer Level). Среди HDL-языков можно выделить Verilog и VHDL ; языки проектирования системного уровня (system-level design languages), позволяющие описывать аппаратную систему на более высоком уровне абстракции и поддерживающие разработку программной части системы. К таким языкам относятся SystemC и SystemVerilog .
В дальнейшем будем называть языками описания аппаратуры или HDL-языками обе разновидности языков.
Рассматриваемые в статье технологии нацелены на автоматизацию разработки тестов для моделей аппаратного обеспечения и на создание тестовых систем с высоким уровнем повторного использования и устойчивых к изменениям реализации.
Перед описанием технологий AVM, OVM и UniTESK (технология URM не описывается в виду почти полного отсутствия документации по ней) отметим следующее. В названии подходов AVM и OVM содержится слово «методология», в то время как UniTESK, по мнению ее создателей, является технологией. В рамках данной статьи мы не различаем эти два термина и понимаем под ними совокупность принципов, методов и инструментов для разработки набора тестов.
Основные принципы AVM
С помощью технологии AVM реализуется возможность разработки сложных тестовых систем на SystemVerilog или SystemC. Основным средством AVM являются библиотеки классов, разработанные на этих языках. При разработке тестовых систем используются следующие базовые принципы: объектно-ориентированный подход, моделирование на уровне транзакций (TLM, Transaction-Level Modeling) и генерация случайных стимулов на основе ограничений (constraint-random generation).
TLM — это подход к моделированию пересылки данных в цифровых системах, при котором организация связи между функциональными модулями отделена от их реализации. Под транзакцией понимается единичная пересылка управляющей информации или данных между двумя модулями. Например, в проектах, использующих шины передачи данных, чтение и запись в шину могут быть описаны транзакциями; в системах с коммутацией пакетов транзакцией является посылка пакета.
Использование объектно-ориентированного подхода и моделирования на уровне транзакций позволяет технологии AVM добиться высоких показателей повторного использования тестов. Использование механизмов наследования и перегрузки методов позволяет переопределять поведение компонента тестовой системы. За счет этого сокращается время, затрачиваемое на разработку и отладку тестов.
Основные принципы OVM
Базовые принципы технологии OVM во многом схожи с AVM. Основным средством OVM является библиотека классов на языке SystemVerilog (в дальнейшем планируется поддержка SystemC), позволяющая создавать модульные тестовые системы, допускающие многократное использование. Одним из достоинств технологии является нацеленность на тестовое покрытие (CDV, Coverage-Driven Verification), что позволяет четко задавать цели тестирования и лучше управлять процессом разработки тестов.
Основные принципы UniTESK
При разработке тестовых систем по технологии UniTESK используются следующие базовые принципы: определенность набора компонентов с ясным разделением функций и четкими интерфейсами; использование формальных спецификаций в форме пред- и постусловий интерфейсных операций и инвариантов типов данных для автоматической генерации тестовых оракулов (компонентов проверки); применение конечно-автоматных моделей для построения последовательностей тестовых воздействий (стимулов).
В качестве основного средства тестирования моделей аппаратного обеспечения используется инструмент CTESK, использующий для разработки тестовой системы язык SeC (Specification extension of C) — расширение языка программирования C.
Тестирование софта - статьи
Аннотация. Работа представляет собой сравнительный анализ современных подходов к разработке функциональных тестов для моделей аппаратуры: AVM (Advanced Verification Methodology) от компании Mentor Graphics, OVM (Open Verification Methodology) — совместной разработки Mentor Graphics и Cadence Design Systems — и технологии UniTESK (Unified TEsting and Specification tool Kit), разработанной в Институте системного программирования РАН. В статье анализируются сильные и слабые стороны различных подходов, сопоставляются архитектуры тестовых систем, даются рекомендации по развитию технологии UniTESK и ее унификации с методологией OVM, набирающей все большее распространение и претендующей на то, чтобы стать стандартом в области тестирования моделей аппаратного обеспечения.
Сравнение технологий разработки тестов
Сравним рассмотренные ранее технологии AVM, OVM и UniTESK. Подходы AVM и OVM разработаны коммерческими организациями с учетом большого опыта тестирования моделей аппаратного обеспечения. Основной акцент в этих технологиях сделан на повторном использовании тестов, которое достигается средствами объектно-ориентированного программирования и моделирования на уровне транзакций. Дополнительно к этому в подходе OVM заложен механизм построения тестовых систем из готовых блоков, отвечающих за тестирование отдельных модулей аппаратной системы. Эта концепция хорошо отражает тенденции современной индустрии, когда основная работа сосредотачивается не на проектировании принципиально нового аппаратного обеспечения, а на интеграции аппаратуры из готовых модулей.
Рисунок 4. Сопоставление архитектур тестовых систем
В технологии UniTESK, являющейся академической разработкой, основной упор сделан на автоматизации создания тестов. В UniTESK используются формальные спецификации поведения в форме пред- и постусловий операций и инвариантов типов данных, а также конечно-автоматные модели для построения последовательностей стимулов. Все это позволяет разрабатывать высококачественные тесты, тщательно проверяющие функциональность тестируемой модели. Из плюсов UniTESK можно также отметить возможность разработки спецификаций с потактовой точностью на основе пред- и постусловий стадий операций. Однако, что касается средств повторного использования тестов, в технологии UniTESK они менее развиты по сравнению с AVM и OVM. Во многом это связано с тем, что инструмент CTESK, используемый для тестирования моделей аппаратного обеспечения, основан на языке программирования C. Реализация основных принципов UniTESK для языков SystemVerilog и SystemC позволила бы улучшить показатели повторного использования тестов.
Сопоставим архитектуру тестовой системы AVM (она такая же, как у OVC-блока) и тестовой системы UniTESK (см. Рис. 4).
Слой транзакторов в тестовой системе AVM приблизительно соответствует слою медиаторов в тестовой системе UniTESK. Соответствие в вышележащих слоях установить сложнее. Генератору стимулов AVM соответствует итератор тестовых воздействий UniTESK (в паре с обходчиком), компонентам проверки — тестовый оракул. Наиболее близким компонентом UniTESK, соответствующим контроллеру тестов AVM, является обходчик. Заметим, что для некоторых компонентов AVM нет явных соответствий в технологии UniTESK, например, там нет таких сущностей, как главные и подчиненные модули.
Сравнительный анализ современных технологий разработки тестов для моделей аппаратного обеспечения
, ,
Труды Института системного программирования РАН
Увеличение сложности аппаратного обеспечения неизбежно
Увеличение сложности аппаратного обеспечения неизбежно влечет за собой развитие технологий разработки тестов. В настоящее время сложность аппаратуры достигла такого уровня, что ее тестирование немыслимо без применения методов автоматизации. Такие методы позволяют разрабатывать тестовые системы, которые автоматически генерируют тестовые последовательности, оценивают правильность поведения системы и собирают информацию о достигнутом уровне тестового покрытия. Однако следует понимать, что автоматизация это далеко не все, что требуется от современной технологии разработки тестов. В условиях постоянного изменения требований и непрерывной доработки проектов огромное значение приобретают такие характеристики технологии, как возможность повторного использования тестов и возможность создания тестов, устойчивых к изменениям реализации. Существующие подходы к построению тестовых систем, такие как AVM (Advanced Verification Methodology), URM (Universal Reuse Methodology), OVM (Open Verification Methodology) и UniTESK (Unified TEsting and Specification tool Kit), в той или иной степени решают обозначенные задачи, но многообразие существующих подходов усложняет взаимодействие между разными группами разработчиков. Стандартизация технологий разработки тестов является необходимым шагом в развитии полупроводниковой индустрии. Появление стандартов создаст предпосылки для отчуждения тестов, что окажет стимулирующее воздействие на рынок готовых компонентов (IPs, Intellectual Property Cores). Если тесты к компоненту аппаратного обеспечения разработаны с использованием общепринятого подхода, сторонние инженеры могут без труда разобраться в них и при необходимости дополнить, а это повышает доверие к компоненту, поставляемому третьей стороной. В последнее время в области тестирования моделей аппаратуры все большее распространение получает технология OVM, совместно разработанная компаниями Mentor Graphics и Cadence Design Systems. Предшественниками OVM являются два основных подхода: AVM (от Mentor Graphics) и URM (от Cadence Design Systems). В данной работе технология OVM вместе со своими предшественниками сравнивается с технологией UniTESK, разработанной в Институте системного программирования РАН. В статье анализируются сильные и слабые стороны указанных подходов, сопоставляются архитектуры тестовых систем, даются рекомендации по развитию инструментов UniTESK и их унификации с подходом OVM. Статья состоит из семи разделов, включая введение и заключение. Во втором разделе вводятся основные понятия, используемые в различных технологиях. Третий, четвертый и пятый разделы посвящены обзору технологий AVM, OVM и UniTESK соответственно. В этих разделах описываются основные принципы и архитектуры тестовых систем для каждого подхода. Шестой раздел содержит сравнительный анализ рассматриваемых технологий. В седьмом разделе делается заключение, в котором даются рекомендации по развитию технологии UniTESK.
в области разработки тестов для
Мы считаем, что в области разработки тестов для моделей аппаратного обеспечения в скором времени должны появиться стандарты. Главным претендентом на звание стандарта является технология OVM, которая продвигается такими крупными компаниями, как Mentors Graphics и Cadence Design Systems. Эта технология основана на хорошо зарекомендовавших себя подходах AVM и URM, поэтому ее начинают активно использовать в индустрии. Мы выступаем за унификацию технологии UniTESK (и других методов автоматизации разработки тестов для моделей аппаратного обеспечения) c подходом OVM. Лучше использовать один подход, который будет понятен разным группам разработчиков. Под унификацией здесь понимается следующее. Основные принципы, на которых основана UniTESK, прежде всего, использование формальных спецификаций в форме пред- и постусловий для описания поведения системы и применение конечно-автоматных моделей для генерации тестовых последовательностей, хорошо зарекомендовали себя на практике. Ничто не мешает реализовать эти принципы в терминах технологии OVM, на основе библиотеки базовых классов. Это позволит создавать тесты по технологии UniTESK, но которые при этом приобретают новое качество — их можно отчуждать, повторно использовать при построении более крупных тестовых систем и т.д.
Алгоритмы уточняющего обхода графов
В технологии тестирования UniTESK тестовая последовательность строится в результате обхода графа состояний обобщенной конечно-автоматной модели целевой системы. Для тестирования в условиях неполной информации мы предлагаем использовать определяемые ниже алгоритмы уточняющего обхода.
Определение. Алгоритмом движения по графу называется алгоритм, который в процессе своей работы строит маршрут в графе.
Определение. Алгоритмом уточняющего движения по графу с уточняемыми вершинами называется алгоритм, который в процессе своей работы строит уточняющий маршрут в графе.
Как и в работе [], будем считать, что алгоритму предоставляются две специальные внешние операции status(), возвращающая идентификатор текущей вершины, и call(x), которая осуществляет переход из текущей вершины по дуге, помеченной стимулом x. Для детерминированного графа такая дуга, если существует, то единственная. Предусловием операции call(x) является допустимость стимула x в текущей вершине. Маршрут строится алгоритмом как последовательность дуг, проходимых последовательными вызовами операции call().
Определение. Для маршрута в графе вершину будем называть пройденной, если этот маршрут содержит хотя бы одну инцидентную ей дугу.
Определение. Для маршрута в графе вершину будем называть завершенной, если этот маршрут содержит все выходящие из вершины дуги.
Определение. Неизбыточным алгоритмом называется алгоритм движения по графу, который зависит только от пройденной части графа и допустимости стимулов в текущей вершине.
Как и в работе [], будем считать, что допустимость стимулов алгоритм может определить с помощью специальной внешней операции next(), которая возвращает стимул, неспецифицированным образом выбираемый среди не выбранных ранее стимулов, допустимых в текущей вершине (осуществляя тем самым итерацию стимулов в вершине). Если все стимулы, допустимые в текущей вершине, уже выбирались, будем считать, что next() возвращает специальный стимул .
Определение. Алгоритмом уточняющего обхода графа называется алгоритм, который в процессе своей работы строит уточняющий обход графа.
Нас будут интересовать только такие алгоритмы, которые останавливаются через конечное число шагов.
Рассмотрим общую схему неизбыточных алгоритмов обхода графов. // пока есть незавершенные вершины while (!сompleted()) { // если текущая вершина незавершена if (next(status()) != ) { // подать очередной стимул call(next(status())); } else { // попасть в пройденную незавершенную вершину rollback(); } }
Операция completed() возврашает true тогда и только тогда, когда в графе все вершины завершены, то есть не существует вершин графа, из которых ведут не пройденные дуги.
Операция rollback() строит маршрут из текущей вершины в вершину, в которой есть еще не пройденные дуги.
Подходы к реализации этой операции могут быть различными. Алгоритмы, основанные на обходе остова графа, выбирают самую дальнюю от корня (поиск в глубину) или самую ближнюю к корню (поиск в ширину) незавершенную вершину, достижимую из текущей []. Другим подходом (жадный алгоритм) является выбор ближайшей достижимой незавершенной вершины, но это требует больших затрат памяти.
Утверждение. Для графов с уточняемыми вершинами, являющихся:
конечными, монотонными, детерминированными, открытыми, сильно-связными
существует неизбыточный алгоритм уточняющего обхода. Доказательство. Рассмотрим следующий алгоритм, точнее его идею, в рамках определенной ранее схемы. Поскольку граф является монотонным, любой маршрут в нем является уточняющим, следовательно, для него определены уровни неопределенности. Алгоритм хранит в памяти некоторую структуру данных, связанных с текущим уровнем неопределенности, например, подобную описанной в работе []. Операция complete() возвращает true тогда и только тогда, когда все пройденные вершины на текущем уровне неопределенности завершены, то есть операция next() для них возвратила ε . Операция rollback() строит маршрут из текущей вершины в незавершенную вершину текущего уровня неопределенности, в которой есть еще не пройденные дуги. Например, это можно сделать на основе остова []. Поскольку различные вершины одного уровня неопределенности несравнимы в отношении уточнения, пройденный на текущем уровне неопределенности граф является подграфом некоторой информационной проекции исходного графа, а следовательно, является детерминированным и сильно-связным что и требуется в []. В случае, если в операции call(x) происходит выбор дуги в вершину, уточняющую одну из вершин текущего уровня неопределенности, текущий уровень неопределенности изменяется, структуры данных освобождаются, алгоритм работает так, как если бы новое состояние было начальным. Поскольку граф конечен, детерминирован и сильно-связен, любая его информационная проекция является конечной, детерминированной и сильно-связной, поэтому внутри любого уровня неопределенности, за исключением последнего, можно гарантированно достичь вершину, в которой допустим стимул, такой что операция call обязательно выберет дугу, выводящую из этого уровня неопределенности.Такие вершина и стимул существуют, поскольку граф является открытым. Таким образом, за конечное число шагов алгоритм достигнет последнего уровня неопределенности, состоящего из полностью определенных вершин исходного графа. Обход которого завершит уточняющий обход исходного графа.
Аннотация
В статье исследуются вопросы функционального тестирования программных систем в условиях неполной информации. Неполнота информации рассматривается в двух аспектах: статическом, связанном с неполнотой функциональных требований, по которым разрабатываются спецификации и тесты, и динамическом, связанном с неполнотой информации о состоянии целевой системы в процессе тестирования. В работе предлагается подход к разработке функциональных спецификаций и генерации функциональных тестов, основанный на использовании неопределенных значений для моделирования состояния целевой системы, а также трехзначной логики Клини для работы с неполными требованиями и описания свойств системы. В качестве базовой технологии используется технология тестирования UniTESK.
Архитектура тестовой системы UniTESK
Архитектура тестовой системы UniTESK была разработана на основе многолетнего опыта тестирования промышленного программного обеспечения из разных предметных областей и разной степени сложности. Учет этого опыта позволил создать гибкую архитектуру, основанную на следующем разделении задачи тестирования на подзадачи. Построение последовательности тестовых воздействий (тестовой последовательности), нацеленной на достижение нужного покрытия. Создание единичного тестового воздействия в рамках тестовой последовательности. Установление связи между тестовой системой и реализацией целевой системы. Проверка правильности поведения целевой системы в ответ на единичное тестовое воздействие.
Для решения каждой из этих подзадач предусмотрены специальные компоненты тестовой системы (см. Рисунок 1): для построения тестовой последовательности и создания единичных тестовых воздействий - обходчик и итератор тестовых воздействий, для проверки правильности поведения целевой системы - оракул, для установления связи между тестовой системой и реализацией целевой системы - медиатор. Рассмотрим подробнее каждый из указанных компонентов.
Обходчик является библиотечным компонентом тестовой системы UniTESK и предназначен вместе с итератором тестовых воздействий для построения тестовой последовательности. В основе обходчика лежит алгоритм обхода графа состояний обобщенной конечно-автоматной модели целевой системы (конечного автомата, моделирующего целевую систему на некотором уровне абстракции). Обходчики, реализованные в библиотеках инструментов UniTESK, требуют, чтобы обобщенная конечно-автоматная модель целевой системы, была детерминированной и имела сильно-связный граф состояний.
Итератор тестовых воздействий работает под управлением обходчика и предназначен для перебора в каждом достижимом состоянии конечного автомата допустимых тестовых воздействий. Итератор тестовых воздействий автоматически генерируется из тестового сценария, представляющего собой неявное описание обобщенной конечно-автоматной модели целевой системы.
Рисунок 1.Архитектура тестовой системы UniTESK.
Оракул оценивает правильность поведения целевой системы в ответ на единичное тестовое воздействие. Он автоматически генерируется на основе формальных спецификаций, описывающих требования к целевой системе в виде пред- и постусловий интерфейсных операций и инвариантов типов данных.
Медиатор связывает абстрактные формальные спецификации, описывающие требования к целевой системе, с конкретной реализацией целевой системы. Медиатор преобразует единичное тестовое воздействие из спецификационного представления в реализационное, а полученную в ответ реакцию - из реализационного представления в спецификационное. Также медиатор синхронизирует состояние спецификации с состоянием целевой системы.
Трасса теста отражает события, происходящие в процессе тестирования. На основе трассы можно автоматически генерировать различные отчеты, помогающие в анализе результатов тестирования.
Генерация тестов на основе неопределенных моделей
Теперь рассмотрим естественное обобщение технологии тестирования UniTESK для генерации тестовых последовательностей на основе неопределенных обобщенных моделей.
В случае, когда состояние модели неопределено, тестовые воздействия можно разделить на три группы: тестовые воздействия, которые допустимы для этого состояния; тестовые воздействия, которые недопустимы для этого состояния; тестовые воздействия, для которых не известно, допустимы они или нет для этого состояния.
Таким образом, итератор тестовых воздействий для каждого обобщенного состояния определяет нечеткое множество тестовых воздействий. Из общих соображений понятно, что чем определеннее обобщенное состояние, тем определенней должен быть набор тестовых воздействий, которые нужно подать в этом обобщенном состоянии, а для полностью определенных обобщенных состояний, набор тестовых воздействий должен быть полностью определен. Обходчик может подавать только те тестовые воздействия, для которых точно известно, что они являются допустимыми в текущем состоянии модели.
В дальнейшем будем предполагать монотонность уточнений состояния целевой системы в процессе тестирования. Это означает, что ни на каком шаге тестирования не происходит потеря информации о состоянии целевой системы, информация может только накапливаться. Монотонность уточнений состояния тесно связана с детерминизмом требований. Пробелы в требованиях, также как и допущения о возможности недетерминированного поведения целевой системы ведут к потере информации в процессе тестирования.
На каждом шаге тестирования тестовая система подает на целевую систему некоторое тестовое воздействие. В ответ на которое, целевая система изменяет свое состояние и выдает реакцию. Используя имеющуюся информацию и полученную реакцию, тестовая система корректирует свое представление о состоянии целевой системы (изменяет и уточняет состояние модели), после чего выносит вердикт о правильности или ошибочности поведения целевой системы. Таким образом, каждый шаг тестирования, с одной стороны, связан с модификацией состояния целевой системы, с другой - с получением дополнительной информации о нем.
В соответствии с традиционным требованием детерминизма обобщенной конечно-автоматной модели в технологии тестирования UniTESK, в нашем случае естественно потребовать детерминизма только в полностью определенных обобщенных состояниях.
Очевидно, что требование детерминизма в не полностью определенных обобщенных состояниях является слишком жестким: неопределенные состояния открыты для уточнения, а возможных уточнений, вообще говоря, может быть несколько. Введем некоторые вспомогательные понятия. Определение. Уточнение состояния целевой системы называется существенным, если оно вызывает уточнение обобщенного состояния. В противном случае, уточнение называется несущественным. После существенного уточнения состояния целевой системы тестовая система переходит на другой информационный уровень. В предположении монотонности уточнений состояния целевой системы, тестовая система больше не вернется в обобщенное состояние, предшествующее существенному уточнению. Определение. Модификация состояния целевой системы называется существенной, если она вызывает изменение обобщенного состояния. В противном случае, модификация называется несущественной. Недетерминизм в существенных модификациях часто означает, что поведение целевой системы зависит от еще не определенной части состояния и, поскольку проверить правильность поведения в этом случае все равно нельзя, тестовая система должна исключать такие тестовые воздействия пока не накопит информацию о состоянии целевой системы, достаточную чтобы вынести вердикт о правильности или ошибочности поведения целевой системы. Последнее требование можно ослабить. Если в процессе тестирования тестовая система перешла в обобщенное состояние, которое является уточнением одного из ранее пройденных обобщенных состояний, это означает, что тестовая система получила дополнительную информацию о состоянии целевой системы, следовательно, тестовую последовательность до настоящего момента можно рассматривать как носящую вспомогательный, уточняющий характер. Вместо традиционного для технологии тестирования UniTESK требования сильной связности графа состояний обобщенной конечно-автоматной модели, естественно потребовать сильной связности для графа обобщенных состояний, расширенного дугами, ведущих из уточняющих обобщенных состояний в уточняемые.Такие дуги вполне естественны, поскольку находясь в некотором обобщенном состоянии, тестовая система в то же время находится и во всех уточняемых им обобщенных состояниях.
Графы с уточняемыми вершинами
В данном разделе вводится понятие графа с уточняющими вершинами, используемое для формального представления неопределенных обобщенных моделей. Вершины графа интерпретируются как обобщенные состояния целевой системы, дуги - как переходы между обобщенными состояниями, а раскраска дуг - как стимулы, инициирующие соответствующие переходы.
Определение. Ориентированным графом или просто графом G называется совокупность трех объектов (GV, GX, GE): GV - множество вершин, GX - множество раскрасок, GE
Определение. Подграф G' = (GV', GX', GE') графа с уточняемыми вершинами G = (GV, GX, GE) называется полностью определенным, если все его вершины полностью определены, то есть GV'
GVc. Определение.
Подграф G' = (GV', GX', GE') графа с уточняемыми вершинами G = (GV, GX, GE) называется его информационной проекцией, если:
вершины из GV' попарно несравнимы в отношении
Строго уточняющий маршрут {(vi, xi, vi+1)}i=0,n-1 в графе с уточняемыми вершинами G называется простым, если никакой его префикс {(vi, xi, vi+1)}i=0,m-1, где m < n, не является строго уточняющим маршрутом. Рассмотрим уточняющий маршрут P = {(vi, xi, vi+1)}i=0,n-1 в графе с уточняемыми вершинами G, начинающийся с неопределенной вершины: v0 =
Инструмент разработки тестов CTesK
Инструмент CTesK является реализацией концепции UniTESK для языка программирования C. Для разработки компонентов тестовой системы в нем используется язык SeC (specification extension of C), являющийся расширением ANSI C. Инструмент CTesK включает в себя транслятор из языка SeC в C, библиотеку поддержки тестовой системы, библиотеку спецификационных типов и генераторы отчетов. Для пользователей Windows имеется модуль интеграции в среду разработки Microsoft Visual Studio 6.0.
Компоненты тестовой системы UniTESK реализуются в инструменте CTesK с помощью специальных функций языка SeC, к которым относятся:
спецификационные функции - содержат спецификацию поведения целевой системы в ответ на единичное тестовое воздействие, а также определение структуры тестового покрытия; медиаторные функции - связывают спецификационные функции с тестовыми воздействиями на целевую систему; функция вычисления обобщенного состояния - вычисляет состояние обобщенной конечно-автоматной модели целевой системы; сценарные функции - описывают набор тестовых воздействий для каждого достижимого обобщенного состояния.
Краткий обзор технологии тестирования UniTESK
Технология тестирования UniTESK [-] была разработана в Институте системного программирования РАН [] на основе опыта, полученного при разработке и применении технологии KVEST (kernel verification and specification technology) []. Общими чертами этих технологий являются использование формальных спецификаций в форме пред- и постусловий интерфейсных операций и инвариантов типов данных для автоматической генерации оракулов (компонентов тестовой системы, осуществляющих проверку правильности поведения целевой системы), а также применение конечно-автоматных моделей для построения последовательностей тестовых воздействий (тестовых последовательностей). В отличие от технологии KVEST, в которой для спецификации требований использовался язык RSL (RAISE specification language) [], технология UniTESK использует расширения широко известных языков программирования.
Литература
| 1.обратно | D. Dibois, H. Prade. Théorie des possibilités. Applications à la representation des connaissances en informatique. MASSON, Paris, Milan, Barselone, Mexico, 1988 (Дюбуа Д., Прад А. Теория возможностей. Приложения к представлению знаний в информатике: Пер. с фр. - М.: Радио и связь, 1990.) |
| 2.обратно | Ю. П. Пытьев. Возможность. Элементы теории и применения. М.: Эдиториал УРСС, 2000. |
| 3.обратно | сайт, посвященный технологии тестирования UniTESK и реализующим ее инструментам. |
| 4.обратно | А. В. Баранцев, И. Б. Бурдонов, А. В. Демаков, С. В. Зеленов, А. С. Косачев, В. В. Кулямин, В. А. Омельченко, Н. В. Пакулин, А. К. Петренко, А. В. Хорошилов. Подход UniTesK к разработке тестов: достижения и перспективы. (Опубликовано .) |
| 5.обратно | В. В. Кулямин, А. К. Петренко, А. С. Косачев, И. Б. Бурдонов. Подход UniTESK к разработке тестов. Программирование, 29(6): 25-43, 2003. |
| 6.обратно | А. Петренко, Е. Бритвина, С. Грошев, А. Монахов, О. Петренко. Тестирование на основе моделей. Открытые системы, №09/2003. (Опубликовано .) |
| 7.обратно | M. Fitting. Kleene's three-valued logics and their children. Fundamenta Informaticae, 20, 113-131, 1994. |
| 8.обратно | сайт Центра верификации операционной системы Linux. |
| 9.обратно | страница инструмента разработки тестов CTesK. |
| 10.обратно | сайт Института системного программирования РАН. |
| 11.обратно | I. Bourdonov, A. Kossatchev, A. Petrenko, and D. Galter. KVEST: Automated Generation of Test Suites from Formal Specifications. FM'99: Formal Methods. LNCS 1708, Springer-Verlag, 1999, pp. 608-621. |
| 12.обратно | The RAISE Language Group. The RAISE Specification Language. Prentice-Hall BCS Practitioner Series. Prentice-Hall, Inc., 1993. |
| 13.обратно | А. В. Хорошилов. Спецификация и тестирование систем с асинхронным интерфейсом. Институт системного программирования РАН, Препринт 12, 2006. |
| 14.обратно | A. Tarski. Introduction to Logic and to the Methodology of Deductive Sciences. New York, 1941. (А. Тарский. Введение в логику и методологию дедуктивных наук. М.: ГИИЛ, 1948.) |
| 15.обратно | Я. А. Слинин. Современная модальная логика. Развитие теории алетических модальностей (1920 - 1960 гг.). Издательство Ленинградского университета, 1976. |
| 16.обратно | И. Б. Бурдонов, А. С. Косачев, В. В. Кулямин. Неизбыточные алгоритмы обхода ориентированных графов. Детерминированный случай. Программирование. т. 29, № 5, стр. 245-258, 2003. |
| 1(обратно) | В дальнейшем эпитет неполный используется в отношении как, собственно, неполной, так и нечеткой информации, как и его синонимы неопределенный и не полностью определенный. |
| 2(обратно) | Часто вместо термина тестирование на основе моделей используется близкий термин тестирование на основе (формальных) спецификаций (specification based testing, specification-driven testing). |
| 3(обратно) | Исключение составляет обходчик ndfsm [], позволяющий обходить графы состояний для некоторого класса недетерминированных конечных автоматов. |
| 4(обратно) | В дальнейшем для краткости будем опускать эпитет функциональные и употреблять термин требования, понимая под ним именно функциональные требования. |
| 5(обратно) | Предполается, что варианты использования целевой системы известны, например, описаны в требованиях к системе. |
| 6(обратно) | На модальные функции возможности и необходимости обычно налагают некоторые ограничения, например, ◊P ≡ ¬ ? ¬ P и ?P ≡ ¬ ◊ ¬ P. |
| 7(обратно) | Обычно модальная логика интерпретируется с помощью системы возможных миров (possible worlds): в каждом возможном мире интерпретация задается двухзначной функцией истинности, а модальные функции определяются совокупностью значений истинности в возможных мирах. |
| 8(обратно) | Возможны и другие варианты определения семантики связок, например, так называемая короткая логика. |
| 9(обратно) | Факторизация задается отношением эквивалентности θ = { (x, y)  |
| 10(обратно) | Здесь для удобства маршрут представлен в виде последовательности вершин. |
| 11(обратно) | В этом случае объем требуемой памяти равен как минимум O(m(log n + X) + nI) вместо O(n(log n + I + X)), где n - число вершин, m - число дуг, I - размер идентификатора вершины, X - размер идентификатора стимула. |
Неопределенность и трехзначная логика Клини
Для не полностью определенных состояний целевой системы, не исключены ситуации, когда из-за недостатка информации некоторые логические условия нельзя отнести ни к истинным, ни к ложным. В таких случаях использование двузначной логики для описания свойств целевой системы представляется не совсем адекватным. Для того чтобы описать логическое условие P, которое может быть неопределенным, с помощью двух значений истинности нужно использовать специальные модальные функции возможности и необходимости: ◊P и ?P и описать условие парой (◊P, ?P). Тогда истинное условие описывается парой (true, true) (необходимо), ложное - парой (false, false) (невозможно), неопределенное - парой (true, false) (возможно, но не необходимо).
Описывать логические условия парой модальностей не очень удобно. Естественней положить, что функция истинности может принимать три значения: true (истина), false (ложь) и
| ◊ | ? | |||
| false | false | false | false | |
| true | true | true | true | |
 | true | | false |
Таблица 1. Определение модальных функций ◊ и ?.
Впервые модальные функции возможности и необходимости подобным образом определил Лукасевич (Lukasiewicz), в трехзначной логике L3 []. В логике L3 неопределенное значение
Подобным образом неопределенное значение интерпретируется в трехзначной логике Клини (Kleene), называемой K3. При получении дополнительной информации значение логического условия может измениться с неопределенного значения
Неопределенные обобщенные модели
Для генерации тестовых последовательностей обычно используют не сами модели тестируемых систем, а их обобщения, называемые обобщенными моделями. Например, в технологии тестирования UniTESK используются обобщенные конечно-автоматные модели, описанные в тестовых сценариях. Поскольку состояния модели могут быть неопределенными, не исключено что и состояния обобщенной модели (обобщенные состояния) окажутся неопределенными.
Пусть M - уточняемый тип, представляющий состояния модели, S - уточняемый тип, представляющий обобщенные состояния, а f: M → S - функция обобщения модели - функция, ставящая в соответствие каждому состоянию модели обобщенное состояние. Будем считать, что функция f является регулярной и полной. В этом случае она задает факторизацию на множестве полностью определенных значений типа M. Для удобства будем считать, что f(
Неопределенные значения и уточняемые типы
Поскольку в процессе тестирования возможна ситуация, когда состояние целевой системы не полностью определено, для моделирования состояния системы удобно использовать типы, поддерживающие неопределенные значения. Будем считать, что на множестве значений типов заданы отношения уточнения, являющиеся отношениями частичного порядка. Отношения уточнения позволяют сравнивать информативность значений: чем «больше» значение в отношении уточнения, тем больше информации оно несет (см. Рисунок 3). Введем несколько понятий.
Рисунок 3.Отношение уточнения значений типа.
Определение. Тип T с заданным на на нем отношением уточнения
Определение. Максимальные значения уточняемого типа T по отношению
T называются (полностью) определенными значениями типа T. Значения уточняемого типа T, не являющиеся полностью определенными, называются неопределенными или не полностью определенными значениями типа T. Определение. Пусть T - уточняемый тип, тогда через Tc будем обозначать (полностью) определенный подтип типа T, то есть подтип, состоящий из всех полностью определенных значений типа T.
Если некоторое свойство P имеет не полностью определенное значение x, это означает, что на самом деле значением свойства P является одно из полностью определенных значений, уточняющих x, но какое именно - неизвестно. Нужно быть аккуратным при сравнении не полностью определенных значений на равенство. С одной стороны, разным неопределенным значениям может соответствовать одно и то же полностью определенное значение, с другой, одному неопределенному значению могут соответствовать разные полностью определенные значения.
Пример.
Рассмотрим пример уточняемого типа ST, представляющего нечеткое множество значений типа T. Нечеткое множество s определяется трехзначной функцией принадлежности fs: T → {true, false,
sT s2 тогда и только тогда, когда из того что fs1(x) = true, вытекает, что fs2(x) = true, а и из того, что fs1(x) = false, вытекает, что fs2(x) = false.
Определение. Пусть T1, …, Tn - уточняемые типы. Определим на декартовом произведении T1× … ×Tn отношение уточнения: (x1, …, xn) T1× ... ×Tn (y1, …, yn) тогда и только тогда, когда x1 T1 y1, …, xn Tn yn. От функций, определенных на уточняемых типах будет требовать регулярности и полноты: чем определеннее значение аргумента, тем определеннее значение функции, причем полностью определенному значению аргумента соответствует полностью определенное значение функции.
Определение. Функция f: T1 → T2 называется регулярной, если из того, что x T1 y следует, что f(x) T2 f(y).
Определение. Функция f: T1 → T2 называется полной, если f(T1с) T2с, то есть из того, что x T1c следует, что f(x) T2c. Обычно в языках программирования и спецификаций есть базовые типы и есть составные типы, значения которых строятся на основе значений других типов. Определение. Составной тип называется регулярным, если все его конструкторы являются регулярными функциями. Определение. Составной тип называется полным, если все его конструкторы являются полными функциями.
Неполнота информации в тестировании
При разработке тестов часто возникает ситуация, когда нет прямого доступа к внутреннему состоянию целевой системы. Такое тестирование называется тестированием со скрытым состоянием (hidden state testing). В отличие от тестирования с открытым состоянием (open state testing), когда состояние целевой системы можно получить непосредственно через ее интерфейс, при тестировании со скрытым состоянием разработчику тестов необходимо четко представлять как изменяется состояние целевой системы при том или ином воздействии на нее. Для возможности определить состояние целевой системы после обработки тестового воздействия важную роль играет детерминизм требований.
Рисунок 2.Виды неполноты информации, возникающие при тестировании.
Другим видом неполноты информации в тестировании является неопределенность начального состояния целевой системы. Такое тестирование называется тестированием с неизвестным начальным состоянием. В отличие от тестирования с известным начальным состоянием, при тестировании с неизвестным начальным состоянием на целевую систему сначала нужно подать последовательность тестовых воздействий, приводящую ее в некоторое известное состояние. Здесь важную роль играют сценарная полнота и детерминизм требований.
Подведем итог относительно различных видов неполноты информации, которые могут возникнуть при тестировании программных систем (см. ). Во-первых, это может быть контрактная неполнота требований. Во-вторых, при тестировании может быть скрыто состояние целевой системы, что не позволяет непосредственно получать состояние целевой системы через ее интерфейс. В-третьих, может быть не определено начальное состояние целевой системы. В-четвертых, требования могут не определять как изменяется состояние целевой системы при выполнении того или иного воздействия или определять это недетерминированным образом. Наконец, реализация целевой системы может быть недетерминированной.
Полнота функциональных требований
В программной инженерии разработка, тестирование, а также сопровождение и эксплуатация программной системы осуществляются на основе требований. На ранних этапах жизненного цикла программной системы требования носят размытый характер, описывая в общих чертах концептуальный замысел разрабатываемой системы. На протяжении всего жизненного цикла системы требования дорабатываются и, пока система используется, их нельзя назвать полностью завершенными. Поскольку в работе исследуются вопросы функционального тестирования, в ней рассматриваются только функциональные требования - требования, описывающие функциональность системы, то есть что она должна делать, но не описывающие как она должна это делать.
Основными свойствами требований, характеризующими их качество, являются понятность, непротиворечивость и полнота. Мы будем рассматривать только одно из них - полноту, предполагая при этом, что требования понятны и непротиворечивы. В дедуктивных науках теория называется полной, если всякое высказывание, сформулированное в терминах этой теории, может быть либо доказано, либо опровергнуто []. В программной инженерии понятие полноты несколько сложнее. Обычно требования рассматриваются в контексте некоторой деятельности и считаются полными, если на их основе можно решить любую задачу в рамках этой деятельности.
Понятно, что из-за различия в роде деятельности, полнота требований по-разному воспринимается разными группами лиц, связанных с программной системой. Например, для пользователя системы полнота требований, в первую очередь, означает возможность на их основе осуществить любой вариант использования системы (use case); для разработчика системы - правильно ее реализовать; для разработчика тестов - разработать полный набор тестов. Поскольку статья посвящена тестированию, полнота требований в ней рассматривается только с точки зрения разработчика тестов.
Простое расширение инструмента CTesK
Для описания предикатов, которые из-за неопределенности состояния целевой системы могут принимать неопределенное значение, предлагается добавить в библиотеку CTesK перечислимый тип Bool3, представляющий значения истинности в трехзначной логике, вместе с основными функциями, реализующими отрицание, дизъюнкцию и конъюнкцию: typedef enum { True_Bool3 = 1, // истина False_Bool3 = 0, // ложь Unknown_Bool3 = -1 // неопределенное значение } Bool3; // отрицание Bool3 not_Bool3(Bool3 arg); // дизъюнкция Bool3 or_Bool3(Bool3 lhs, Bool3 rhs); // конъюнкция Bool3 and_Bool3(Bool3 lhs, Bool3 rhs);
Для удобства работы со значениями типа Bool3 также в библиотеку CTesK можно добавить модальные функции возможности и необходимости: // модальная функция возможности bool may_Bool3(Bool3 arg); // модальная функция необходимости bool shall_Bool3(Bool3 arg);
Для задания отношения уточнения на множестве значений спецификационных типов предлагается добавить в спецификационные типы поле .refines, которое можно инициализировать функцией вида: bool refines(Object *lhs, Object *rhs);
Функция возвращает значение true тогда и только тогда, когда спецификационный объект rhs уточняет спецификационный объект lhs.
Используя функцию refines(), обходчики в процессе построения тестовой последовательности могут учитывать изменения уровня неопределенности, тем самым подавая вспомогательные инициализирующие тестовые воздействия, которые сейчас приходится писать вручную.
Поскольку значение, возвращемое постусловием спецификационной функции, имеет двузначный логический тип, а определить правильность или ошибочность поведения целевой системы в условиях неполной информации не всегда возможно, предлагается при определении структуры тестового покрытия выделять специальные ветви функциональности Unknown: { "Описание ветви функциональности", Unknown };
Выделенные ветви функциональности описывают ситуации, в которых оракул тестовой системы не обладает достаточной информацией, чтобы вынести однозначный вердикт о правильности или ошибочности поведения целевой системы. При попадании в одну из таких ветвей можно не проверять постусловие. Так как ветви Unknown носят вспомогательный характер, информация об их покрытии не должна попадать в отчеты о достигнутом покрытии.
Если после выполнения теста некоторые ветви функциональности, отличные от Unknown, оказались непокрытыми, это может быть связано со сценарной неполной требований. Возможно, что требования не определяют как достичь или идентифицировать соответствующие тестовые ситуации. Предположим, что оракул в качестве вердикта может возвращать неопределенное значение. Если после выполнения теста для некоторых ветвей функциональности вердикт оказывается неопределенным, это может быть связано с контрактной неполнотой требований. Цель тестирования - покрыть все ветви функциональности, вынеся при этом определенные вердикты, и достижение этой цели как правило связано с уточнением требований к целевой системе.
Простое расширение технологии UniTESK
Рассмотрим как можно расширить технологию тестирования UniTESK средствами тестирования в условиях неполной информации на примере инструмента разработки тестов CTesK []. В своих предложениях по расширению мы руководствовались тем соображением, что трудоемкость расширения должна быть минимальной.
Спецификация в условиях неполной информации
В данном разделе рассматривается подход к разработке функциональных спецификаций, позволяющий работать с неполными требованиями к целевой системе и неполной информацией о ее состоянии.
Тестирование в условиях неполной информации. Подход к разработке спецификаций и генерации тестов
А. С. Камкин,
Труды Института системного программирования РАН
Как уже неоднократно отмечалось, при тестировании возможна ситуация, когда информация о состоянии целевой системы не доступна полностью тестовой системе. Это означает, что соответствующее состояние модели не полностью определено. В данном разделе описывается подход к генерации тестовых последовательностей, позволяющий работать в таких условиях.
Требования и оценка правильности поведения системы
Теперь рассмотрим определение полноты требований в контексте разработки спецификаций. Одна из основных задач разработчика тестов - определить, какое поведение целевой системы следует считать правильным, а какое ошибочным. Ясно, что требования, претендующие на полноту, должны позволять проводить такую классификацию.
Определение. Будем говорить, что требования к целевой системе являются контрактно полными, если на их основе можно однозначно классифицировать поведение целевой системы на правильное или ошибочное на любом допустимом сценарии взаимодействия с ней. В противном случае будем говорить, что требования являются контрактно неполными.
Контрактная неполнота требований означает, что в оракуле, оценивающем поведение целевой системы, есть «дыры» - возможны ситуации, в которых он не может вынести однозначный вердикт о правильности или ошибочности поведения целевой системы.
Проиллюстрируем понятие контрактной полноты требований на следующем примере.
Пример. Рассмотрим целевую систему из предыдущего примера. Пусть требования к функции pop() формулируются следующим образом: Вызов функции pop для непустого стека возвращает последний добавленный в него элемент.
Эти требования не являются контрактно полными, так как в них не описано, как должна вести себя функция pop для пустого стека. Если добавить в требования описания того, что вызов функции pop для пустого стека должен возвратить NULL, требования становятся контрактно полными.
Требования и сценарии взаимодействия с системой
Задачу тестирования можно разбить на две основные подзадачи: построение последовательности тестовых воздействий и проверку правильности поведения целевой системы в ответ на поданные тестовые воздействия. В соответствии с этим, разработка тестов по технологии UniTESK разбивается на разработку тестовых сценариев и разработку спецификаций. Данный раздел посвящен определению полноты требований для разработки тестовых сценариев.
Определение. Будем говорить, что требования к целевой системе являются сценарно полными, если они описывают, как на основе интерфейса целевой системы можно реализовать все указанные в них варианты использования, а также воссоздать или идентифицировать все указанные в них ситуации.
В сценарно неполных требованиях для некоторых описанных в них ситуаций могут отсутствовать описания способов их достижения или идентификации. В контексте технологии тестирования UniTESK это означает невозможность достичь 100% покрытия тестовых ситуаций, определенных в спецификации на основе требований. Если требования сценарно неполны, значения некоторых атрибутов состояния спецификации оказываются неопределенными на любых последовательностях тестовых воздействий.
Определение. Будем говорить, что требования к целевой системе являются детерминированными, если они описывают, как на основе интерфейса целевой системы можно контролировать или наблюдать ее поведение при выполнении всех возможных сценариев взаимодействия с ней. В противном случае будем говорить, что требования являются недетерминированными.
Если требования недетерминированны, то возможны сценарии взаимодействия с целевой системой, при выполнении которых нельзя однозначно определить состояние целевой системы. В контексте технологии тестирования UniTESK это означает, что функция вычисления постсостояния спецификации в некоторых ситуациях оказывается недетерминированной.
Проиллюстрируем понятие сценарной полноты и детерминизма требований на следующем простом примере.
Пример. Целевая система является стеком.
Интерфейс целевой системы состоит из следующих функций:
Stack* create(void); void push(Stack *stack, Object *obj); Object* pop(Stack *stack).
Пусть требования к целевой системе формулируются следующим образом:
Функция create создает пустой стек и возвращает указатель на него. В случае, если стек не полностью заполнен, вызов функции push добавляет в него элемент, противном случае, вызов функции push не меняет состояние стека. Вызов функции pop для непустого стека возвращает последний добавленный в него элемент, для пустого стека - NULL.
Эти требования не являются сценарно полными, так как не описывают как достичь или идентифицировать указанную в них ситуацию «стек полностью заполнен». Также эти требования не являются детерминированны, так как не позволяют однозначно определить в какое состояние перейдет целевая система после вызова функции push. Если добавить в требования описание ситуации «стек полностью заполнен», указав, например, максимальное возможное число элементов в стеке, требования становятся сценарно полными и детерминированными.
и широко распространяются методы, оперирующие
В последнее время в науке и технике интенсивно развиваются и широко распространяются методы, оперирующие с неполной или нечеткой информацией []. Примерами теорий, в рамках которых разрабатываются подобные методы, являются математическая статистика, теория нечетких множеств, теория возможностей и многие другие. Методы анализа и обработки неполной информации хорошо зарекомендовали себя в искусственном интеллекте, теории баз данных, системном анализе и исследовании операций. Сегодня их активно используют для моделирования сложных физических, экономических и социальных явлений []. Таким образом, работа с неопределенной и нечеткой информацией постепенно становится уделом точных наук. Программной инженерии, претендующей на точность и методичность инженерной дисциплины, также приходится иметь дело с неполной информацией. В проектах по разработке программного обеспечения неопределенность возникает на самых ранних фазах. Размытый и туманный характер носят требования к программной системе, которые приходится многократно уточнять, дополнять и согласовывать. После доработок требования используются на следующей фазе, на которой, как правило, имеют дело с более низким уровнем абстракции, поэтому требования вновь кажутся неполными, их снова приходится дорабатывать. Таким образом, на каждой фазе проекта исходная информация оказывается не полностью определенной. В работе рассматривается лишь один из этапов разработки программного обеспечения - тестирование. Обычно на этапе тестирования располагают более-менее завершенным продуктом и достаточно проработанными требованиями. Казалось бы, что на этом этапе в требованиях не должно быть никаких неопределенностей, но, как показывает практика, это не так. Использование требований для целей тестирования в очередной раз выявляет их недостатки. Требования после многочисленных доработок вновь оказываются неполными. С другой стороны, в процессе тестирования возможна ситуация, когда состояние целевой системы не полностью определено. Например, такая ситуация может возникнуть, когда состояние целевой системы скрыто, а начальное состояние в требованиях не определено.
Неполнота информации о состоянии целевой системы может приводить к невозможности адекватной оценки правильности поведения целевой системы. Перед тем, как оценивать поведение, необходимо получить представление о состоянии целевой системы путем подачи тестовых воздействий и анализа реакций на них. Статья выполнена в контексте тестирования на основе моделей (MBT, model based testing), более точно, в контексте технологии тестирования UniTESK [-], хотя рассматриваемые в ней вопросы актуальны не только для этой технологии. Модель представляет собой некоторое достаточно абстрактное отображение структуры и поведения целевой системы, созданное на базе требований []. В процессе тестирования состояние модели можно интерпретировать, как располагаемую информация о состоянии целевой системы, сформулированную в терминах требований. В работе предлагается подход к разработке функциональных спецификаций и генерации функциональных тестов, позволяющий работать с неполными требованиями к целевой системе и неполной информацией о ее состоянии. Подход основан на использовании неопределенных значений для моделирования состояния целевой системы, а также трехзначной логики Клини (Kleene) [] для работы с требованиями и описания свойств системы. Результаты работы получены в ходе выполнения проекта по разработке открытого тестового набора OLVER для операционной системы Linux []. Статья построена следующим образом. Во втором, следующем за введением, разделе делается краткий обзор технологии тестирования UniTESK. В третьем разделе рассматриваются вопросы, связанные с неполнотой функциональных требований и неполнотой информации о состоянии целевой системы в процессе тестирования. В четвертом разделе описывается подход к спецификации систем на основе неопределенных значений, уточняемых типов и трехзначной логики Клини. В пятом разделе рассматриваются вопросы построения тестовых последовательностей по неопределенным обобщенным моделям. В шестом разделе предлагается простое расширение технологии тестирования UniTESK на примере инструмента разработки тестов CTesK [].В заключении делается краткое резюме работы.
В работе были рассмотрены вопросы
В работе были рассмотрены вопросы функционального тестирования программных систем в условиях неполной информации. На базе технологии тестирования UniTESK предложен подход к разработке функциональных спецификаций и генерации функциональных тестов, основанный на использовании неопределенных значений для моделирования состояния целевой системы, а также трехзначной логики Клини для работы с неполными требованиями и описания свойств системы. Идеи предложенного подхода нашли свое применение в проекте по разработке открытого тестого набора OLVER для операционной системы Linux.
Абстрактное состояние
Абстрактное состояние – это множество структур данных, которые моделируют внутреннее состояние целевой системы. Все действия, которые выполняет целевая система, моделируются в терминах абстрактного состояния.
Документация на IPv6 не содержит требований к внутреннему устройству реализации IPv6. Абстрактное состояние было спроектировано таким образом, чтобы предоставить удобные концептуальные структуры данных для спецификаций стимулов и реакций.
Абстрактное состояние для MSR IPv6 включает следующие элементы:
Множество исходящих пакетов IPv6. Это множество моделирует множество пакетов, которые реализация передает канальному уровню Набор очередей входящих датаграм UDP. Данные очереди используются для моделирования получения данных клиентами UDP. Пул фрагментов. Пул фрагментов используется для двух целей. (1) мы моделируем процедуру сборки пакетов в целевой системе. (2) мы проверяем, что из фрагментов, которые выпускает целевая система, получатель сможет воссоздать оригинальный пакет Набор таблиц Neighbor Discovery. Эти таблицы используются при моделировании алгоритмов Neighbor Discovery.
Функции IPv выбранные для тестирования
Для тестирования мы выбрали минимальное подмножество функций IPv6, которое обеспечивает корректное функционирование оконечного узла (host).
ICMPv6 – это протокол, который используется для передачи служебных сообщений на сетевом уровне. В частности, форматом пакетов ICMPv6 пользуются протоколы Neighbor Discovery (см. далее). Протокол ICMPv6 специфицирован в RFC 2463 . Кроме того, ICMPv6 используется некоторыми протоколами верхнего уровня (например, UDP), для передачи сообщений об ошибках. ICMPv6 Echo
ICMPv6 Echo – это простой диагностический протокол, который используется для определения пропускной способности сети и состояния удаленного узла IPv6. В частности, данный протокол использует утилита ping. Протокол ICMPv6 Echo является неотъемлемой частью ICMPv6 и определен также в RFC 2463 . Протокол использует формат пакетов ICMPv6. Всего в протоколе два вида сообщений – Echo Request и Echo Reply. При получении Echo Request узел IPv6 должен выслать ответ, Echo Reply, тому узлу, от которого пришел запрос. Таким образом, узел – источник запроса – может установить, что адресат запроса достижим. Если же узел-источник не получит ответа, то либо узел-адресат не функционирует, либо сеть перегружена и не в состоянии доставить пакет адресату. При тестировании мы проверяли, что реализация корректно строит пакеты-запросы Echo Request, и выдает корректные ответы (Echo Replies) на корректные запросы Echo Request.
Тестовый набор разрабатывался средствами реализации
Тестовый набор разрабатывался средствами реализации UniTesK для языка С – CTesK-lite. CTesK-lite поддерживает разработку спецификаций на спецификационном расширении языка С – SEC (Specification Extension of C language). В CTesK-lite реализована архитектура тестового набора UniTesK – тестовые сценарии, оракулы, медиаторы. Реализована поддержка тестирования систем с отложенными реакциями. SEC – это ASCII C, к которому были добавлены ряд конструкций, характерных для академических языков формальных спецификаций. В частности, в SEC реализованы пред- и пост- условия, инварианты типов данных и глобальных переменных, описатели доступа (access descriptors). Из спецификаций на языке SEC генерируется код на языке С, который затем компилируется обыкновенным компилятором С (в нашем случае MS VC 6.0). Для разработки и сборки тестового набора мы использовали MS Visual Studio 6.0. Проверка синтаксиса и семантики для SEC не реализована, но синтаксические ошибки в спецификациях можно идентифицировать по ошибкам, которые компилятор С находит в сгенерированном коде. Далее в данном разделе приведены краткие описания компонентов тестового набора.
Литература
Information technology -- Open Systems Interconnection -- Basic Reference Model. ISO/IEC 7498, 1994 S. Deering, R. Hinden. Internet Protocol, Version 6 (IPv6) Specification. RFC 2460, December 1998 M. Crawford. Transmission of IPv6 Packets over Ethernet Networks. RFC 2464, December 1998 A. Conta, S. Deering. Internet Control Message Protocol (ICMPv6) for the Internet Protocol Version 6 (IPv6) Specification. RFC 2463, December 1998 T. Narten, E. Nordmark, W. Simpson. Neighbor Discovery for IP Version 6 (IPv6). RFC 2461, December 1998 http://research.microsoft.com/msripv6/ R. P. Draves, A. Mankin, B. D. Zill. Implementing IPv6 for Windows NT. Proceedings of the 2nd USENIX Windows NT Symposium, Seattle, WA, August 3–4, 1998 I. Bourdonov, A. Kossatchev, V. Kuliamin, A. Petrenko. UniTesK Test Suite Architecture. Proceedings of FME 2002. LNCS 2391, pp. 77-88, Springer-Verlag, 2002. I. Bourdonov, A. Kossatchev, A. Petrenko, D. Galter. KVEST: Automated Generation of Test Suites from Formal Specifications. FM’99: Formal Methods.LNCS, volume 1708, Springer-Verlag, 1999, pp. 608–621. И. Б. Бурдонов, А. В. Демаков, А. С. Косачев, А. В. Максимов, А. К. Петренко. Формальные спецификации в технологиях обратной инженерии и верификации программ. Труды Института системного программирования, 1999 г., том 1, стр. 35-47 И.Б.Бурдонов, А.С.Косачев, В.В.Кулямин. Асинхронные автоматы: классификация и тестирование. В данном сборнике I.Agamirzian, S.G.Groshev, A.V.Khoroshilov, G.N.Kluchnikov, A.S.Kossatchev, V.A.Omelchenko, N.V.Pakoulin, A.K.Petrenko, V.Z. Shnitman. MSR IPv6 verification project. Technical report, December 2001
Медиаторы
По медиаторами в UniTesK понимают промежуточный слой между оракулами и реализацией.
Необходимость введения медиаторов вызвана тем, что в UniTesK воздействия на целевую систему и реакции целевой системы описываются в терминах модели, содержащейся в спецификациях. Перед тем как оказать воздействие на целевую систему, необходимо перевести параметры воздействия из модельного представления в представление реализации, а после того, как воздействие оказано, необходимо перевести реакции целевой системы в модельное представление. Также необходимо отобразить изменения состояния целевой системы в абстрактном состоянии.
В UniTesK медиаторы осуществляют необходимые преобразования, оказывают воздействия на целевую систему и собирают реакции целевой системы.
Как упоминалось выше, в интерфейс целевой системы входят непроцедурные стимулы – пакеты IPv6, которые поступают в целевую систему из сети. Медиатор для непроцедурных стимулов представляет собой распределенное приложение, реализованное в рамках архитектуры клиент-сервер. Клиент – тестовая система – передает серверу запрос, в котором содержится IPv6 пакет адрес узла назначения. Сервер, который работает на некотором узле в том же сегменте сети, что и целевой узел, пересылает указанный пакет по указанному IPv6 адресу. Для того, чтобы обмен запросами между клиентом и сервером не оказывал воздействия на целевую систему, запрос серверу передается по сети IPv4.
Тестовая система работает на том же компьютере, что и целевая система. Благодаря этому медиаторы для процедурных стимулов устроены просто. Медиатор для отправки датаграммы UDP вызывает процедуру sendto для отправки указанных данных по указанному адресу через указанный сокет. После того, как sendto возвращает управление, медиатор анализирует возвращенное значение и, при необходимости, код ошибки и формирует собственное возвращаемое значение (OK/FAIL). Медиатор для функции Echo Request обращается к соответствующей точке доступа транспортного драйвера MSR IPv6. После завершения вызова медиатор анализирует возвращенное значение и, при необходимости, код ошибки, сохраняет данные ответа (Echo Reply) и формирует собственное возвращаемое значение (OK/FAIL)
Neighbor Discovery (ND) объединяет группу протоколов, которые решают следующие задачи:
Определение адресов канального уровня для узлов, которые располагаются на одном сегменте локальной сети (соседей) Определение маршрутизаторов, которые подсоединены к сегменту локальной сети Определение того, через какой маршрутизатор отправлять пакеты, адресованные узлам за пределами сегмента локальной сети
Для сбора информации о соседних узлах узел IPv6 отправляет и получает служебные пакеты. Всего в ND на данный момент насчитывается пять видов служебных пакетов. Все пакеты используют формат пакетов ICMPv6. Протокол ND задан в RFC 2461 Для уменьшения нагрузки на сеть собранная информация сохраняется узлом, поэтому на протоколы ND возлагается задача своевременно обновлять сведения соседних узлах и удалять устаревшие записи. При тестировании мы проверяли, что реализация правильно обновляет информацию о соседях, правильно выбирает маршрутизаторы для отправки пакетов за пределы локальной сети, правильно сообщает информацию о себе соседям.
Для точного определения покрытия кода целевой системы необходимо пропустить тесты на отладочной версии ядра Windows 2000 с включенным профилировщиком ядра. Это сделано не было, поэтому оценка покрытия кода получена косвенным методом. Мы составили список всех процедур, которые есть в целевой системе, и для каждой процедуры оценили, будет ли она вызываться при прогоне тестов. Оказалось, что 20% процедур в целевой системе не будут вызываться при прогоне тестов; как правило, эти процедуры реализуют функции IPv6, исключенные из рассмотрения при разработке тестового набора. 60% процедур реализуют выбранные нами функции IPv6; эти процедуры должны вызываться при пропуске тестов. Про остальные 20% мы затрудняемся сказать что-либо определенное; как правило, это вспомогательные процедуры. Итого получается оценка покрытия исходных текстов 60-80%.
Оракулы – это процедуры, которые проверяют выполнение ограничений, наложенных на поведение целевой системы. В UniTesK оракулы полностью автоматически генерируются из описаний ограничений. В UniTesK ограничения описаны преимущественно в форме имплицитных спецификаций стимулов и реакций. Кроме того, часть ограничений представлены в виде ограничений на значения типов (инварианты типов) и ограничений на значения глобальных переменных (инварианты глобальных переменных). Имплицитные спецификации состоят из пред- и пост- условий. Предусловие содержит требования к тому, в каком состоянии и с какими параметрами можно оказывать воздействие на целевую систему. После воздействия целевая система может продемонстрировать реакции и/или перейти в другое состояние. Постусловие определяет, допустимо ли изменение состояния и продемонстрированное поведение целевой системы. Состояние целевой системы моделируется набором структур данных, которые получили название абстрактное состояние. Пред- и постусловия используют информацию, содержащуюся в абстрактном состоянии, для вынесения вердикта.
Протокол обеспечивает обмен данными между протоколами более высокого уровня. Также протокол производит обмен служебными сообщениями сетевого уровня между узлами. Формат пакетов IPv6 и правила обработки пакетов определены в RFC 2460 . При отправке пакета протокола верхнего уровня IPv6 формирует свой собственный пакет, включает в него заданный пакет верхнего уровня, и передает полученный пакет IPv6 в сеть. При тестировании мы проверяем, что реализация формирует корректные пакеты IPv6, и данные протокола верхнего уровня передаются в сеть без искажений. При получении пакета из сети реализация IPv6 разбирает пакет. В том случае, если в пакет содержит ошибки, то реализация пакет отбрасывает или отправляет источнику пакета сообщение об ошибке. Если же пакет корректен, то реализация определяет протокол верхнего уровня, которому адресованы данные, содержащиеся в пакете, и передает их получателю. При тестировании мы проверяем поведение реализации как на корректных пакетах, так и на некорректных пакетах. Фрагментация и сборка пакетов.
Большинство протоколов канального уровня накладывают ограничения на размер передаваемых данных. Так, в сети Ethernet максимальный размер пакета сетевого уровня, который передается в одном кадре Ethernet, равен 1500 байт. Для передачи больших массивов данных в IPv6 предусмотрена функция фрагментации пакетов. В том случае, если размер пакета протокола верхнего уровня превосходит максимальный допустимый размер, то реализация IPv6 пересылает такой пакет по частям. Реализация нарезает данные на фрагменты и отправляет каждый фрагмент в отдельном пакете. В точке назначения фрагменты накапливаются и по получению всех фрагментов из них восстанавливается первоначальный пакет. Фрагментация и сборка пакетов происходит прозрачно для протоколов верхнего уровня. При тестировании мы проверяли, что реализация протокола корректно строит фрагменты, корректно восстанавливает данные из последовательности фрагментов, а также надежно обрабатывает ошибки во фрагментах и сериях фрагментов. Именно в функции сборки фрагментов мы обнаружили наиболее серьезный дефект в MSR IPv6, который приводит к перезагрузке операционной системы.
Как сказано выше, целевая система может демонстрировать реакции спустя некоторое время после того, как на неё было оказано воздействие. Мы называем такое поведение отложенными реакциями. Как правило, неудобно моделировать отложенные реакции посредством обычных конечных автоматов. Для облегчения моделирования систем с отложенными реакциями в UniTesK введено представление об автоматах с отложенными реакциями . Автоматы с отложенными реакциями отличаются от обычных конечных автоматов тем, что переходы в между состояниями представляют собой цепочку реакций. Как правило, целевая система демонстрирует реакции нескольких различных видов. Например, у реализации сетевого протокола есть как минимум два вида реакций – пакеты, которые отправляется в сеть, и пакеты, которые передаются на верхний уровень. Для регистрации отложенных реакций целевой системы тестовая система содержит так называемые кетчеры. Кетчеры, как видно из названия, “хватают” (catch) реакции целевой системы и передают их в тестовую систему. В тестовой системе должны быть кетчеры для каждого вида реакций. Реакции могут регистрироваться с запозданием, причем для реакций различных типов величина задержки может быть различной. Тестовой системе необходимо определить допустимый порядок реакций различных видов. Процедура определения допустимой последовательности реакций называется сериализацией. В процессе сериализации тестовая система строит различные цепочки реакций и проверяет их допустимость. Каждая реакция рассматривается как переход между промежуточными состояниями, конечное состояние последней реакции рассматривается как последнее состоянии в цепочке реакций и принадлежит множеству состояний конечного автомата. Если при сериализации не удалось найти ни одной допустимой последовательности реакций, то тестовая система выносит вердикт о рассогласовании модели и целевой системы – набор зарегистрированных реакций не соответствуют спецификации. Сериализация реакций происходит после того, как все реакции целевой системы получены.
Процесс разработки тестового набора для MSR IPv6 можно разделить на несколько фаз:
Определение интерфейса Разработка спецификаций для отправки и получения пакетов без Neighbor Discovery Разработка и прогон тестовых сценариев для отправки и получения пакетов без Neighbor Discovery Пополнение спецификаций функцией Neighbor Discovery. Разработка и прогон тестовых сценариев для Neighbor Discovery Прогон всего полученного тестового набора
На фазе определения интерфейса был определен состав функций IPv6 для тестирования, и определены стимулы и реакции, относящиеся к выбранным функциям. Разработка спецификаций проводилась в два этапа. На первом этапе были разработаны спецификации, в которых не моделировалось поведение Neighbor Discovery. Для полученных спецификаций были разработаны и отлажены тестовые сценарии. Протоколы Neighbor Discovery предназначены для сбора и обновления информации о конфигурации сегмента локальной сети, к которой подключен узел IPv6. В спецификациях и тестовых сценариях, которые мы разработали на первом этапе, конфигурация сети предполагалась заданной и неизменной во времени. Это предположение позволило разработать и отладить довольно содержательные тестовые сценария для функций отправки и получения пакетов и ICMPv6. На втором этапе мы добавили спецификации протоколов Neighbor Discovery. Для отладки полученных спецификаций мы воспользовались предположением, что сценарии, разработанные для спецификаций без ND, должны корректно работать и для спецификаций с ND. Избранная нами стратегия себя оправдала. При прогоне тестовых сценариев, разработанных на первом этапе, было выявлено и исправлено много недочетов в спецификациях Neighbor Discovery. После того, как спецификации Neighbor Discovery были отлажены, были разработаны тестовые сценарии специально для Neighbor Discovery.
MSR IPv6 отличает хорошая структуризация исходных текстов. Код, который реализует некоторую функцию IPv6, как правило сгруппирован в отдельные файлы, и может рассматриваться как отдельная подсистема MSR IPv6. На рисунке 1 представлено разбиение MSR IPv6 на подсистемы. В средней части рисунка представлены подсистемы, которые реализуют базовые функции IPv6 – отправка и получение пакетов, ND, ICMPv6. Прямоугольник, помеченный как “Routing”, реализует часть функций Neighbor Discovery, которые относятся к работе с маршрутизаторами. В верхней части рисунка представлены транспортные протоколы, реализации которых есть в MSR IPv6 – TCP и UDP. В нижней части рисунка расположены подсистемы, которые обеспечивают взаимодействие IPv6 с протоколами нижнего уровня (LAN) и псевдоустройством закольцованной связи (loopback).
Был разработан тестовый набор для реализации протокола IPv6. Тестовый набор был пропущен на Windows 2000, в качестве целевой системы выступала реализация IPv6 от Microsoft Research (MSR IPv6 version 1.4). Проект по разработке тестового набора для MSR IPv6 показал применимость UniTesK для тестирования сложного API с непроцедурными стимулами и отложенными реакциями. Также показана применимость UniTesK для тестирования внутренних подсистем ядра Windows 2000. В ходе тестирования были обнаружены отклонения от стандартов IPv6 и ошибки программирования. Отклонения от стандартов заключаются в том, что в ряде случаев поведение MSR IPv6 отличается от требований, изложенных в стандартах на IPv6. При тестировании мы выявили также дефекты, которые можно охарактеризовать как ошибки, допущенные при программировании.
Сбор реакций целевой системы осуществляют специальные программы, которые называются кетчерами (от английского глагола to catch – ловить). Как было сказано выше, MSR IPv6 демонстрирует два вида отложенных реакций – исходящие IPv6 пакеты и UDP датаграммы, которые получают в сокетах. Входящие и исходящие пакеты IPv6
Кетчер для входящих/исходящих пакетов IPv6 перехватывает кадры Ethernet, в которых передаются пакеты IPv6. Кетчер реализован как модуль расширения Microsoft Network Monitor’а. Кетчер не разбирает кадры Ethernet, а передает их в тестовую систему. Заметим, что кетчер не умеет отличать исходящие кадры от входящих. В тестовой системе перехваченные кадры преобразуются. Тестовая система извлекает из кадра вложенный в него пакет IPv6 и определяет, является пакет входящим или исходящим. При этом формируется специальная структура данных, которая используется в спецификациях для представления пакетов IPv6. Входящие датаграммы UDP
При старте тестовая система открывает несколько сокетов и запускает кетчер, которая слушает открытые сокеты. Когда в один из сокетов прибывает датаграмма, кетчер получает датаграмму и определяет исходный адрес датаграммы.
Спецификации можно рассматривать как формальное представление требований к целевой системе. В наших спецификациях мы формализовали требования, взятые из стандартов IPv6. В основном, требования извлекались из , но использовались также ряд других RFC. Спецификации представляют собой формализованную запись требования, изложенных в RFC. Для того, чтобы сохранить прослеживаемость требований в тесте спецификаций расставлялись ссылки на соответствующие полуформальные требования из RFC. Благодаря этому по расхождениям между реализацией и моделью, выявленным при прогоне тестов, можно определить, какое требование из RFC нарушено в реализации.
MSR IPv6 демонстрирует два вида отложенных реакций - исходящие пакеты IPv6 и входящие пакеты UDP, то есть данные, которые получают клиенты протокола UDP. Кроме того, по техническим причинам мы моделировали входящие пакеты IPv6 также как реакции (см. обсуждение выше). Спецификация для исходящих пакетов IPv6 проверяет следующее:
Все пакеты, которые целевая система отправляет в сеть, удовлетворяют требованиям на формат пакетов, изложенным в соответствующих RFC. Все фрагменты, которые целевая система отправляет в сеть, можно собрать в пакет IPv6 Корректность данных для некоторых видов пакетов (например, UDP и ICMPv6)
Спецификация для входящих пакетов IPv6 разбирает входящие пакеты IPv6. Если в пакете нет ошибок, то спецификация определяет получателя данного пакета и моделирует получение данных пакета получателем. Если в пакете обнаружена ошибка, то спецификация определяет, какое сообщение об ошибке следует послать. Спецификация для входящих пакетов IPv6 также моделирует сборку пакетов из фрагментов. В спецификации восстанавливается исходный пакет и моделируется доставка восстановленного пакета получателю. Спецификация для входящих датаграм UDP проверяет, что датаграмма получена в правильном сокете и данные получены без искажений.
Функция фрагментации формально относится к функции отправки пакета в сеть. Тем не менее, спецификация стимулов не описывает фрагментацию. Проверка правильности фрагментации возложена на спецификацию для исходящих пакетов. Данная спецификация проверяет, что из фрагментов можно собрать оригинальный большой пакет, собирает большой пакет и затем проверяет, что полученный пакет соответствует одному из пакетов, которые были созданы по запросу протокола верхнего уровня.
Подсистема Neighbor Discovery не содержит входных точек, доступных извне модуля MSR IPv6. ND обрабатывает входящие пакеты и сохраняет информацию о соседних узлах во внутренних таблицах. При отправке IPv6 пакета в сеть соответствующая подсистема IPv6 запрашивает у ND информацию об узле назначения пакета. В результате такого запроса ND может выслать один или более служебных пакетов. Спецификация для входящих пакетов распознает пакеты Neighbor Discovery и определяет, какая информация должна сохраняться в таблицах Neighbor Discovery. Спецификация для исходящих пакетов IPv6 проверяет следующее:
Реализация отправляет пакеты известным узлам Реализация производит поиск соседа перед отправкой пакетов незнакомым соседним узлам Реализация не отсылает пакеты, если Neighbor Discovery не в состоянии найти узел адресат Реализация правильно определяет, какие узлы находятся на том же сегменте локальной сети, а какие находятся вне сегмента локальной сети Реализация находит маршрутизаторы в локальной сети и корректно обновляет информацию о маршрутизаторах
Заметим, что спецификация не старается предсказать, на какой узел локальной сети будет выслан пакет. Вместо этого спецификация проверяет, что узел, выбранный реализацией, соответствует информации, собранной Neighbor Discovery на момент отправки пакета.
Алгоритм обхода графа состояний автомата тестового сценария, реализованный в CTesK-lite, требует, чтобы воздействия на целевую систему оказывались только в стационарных состояниях. Протокол IPv6 не удовлетворяет указанному ограничению, так как некоторые внешние воздействия (входящие пакеты) могут оказываться в нестационарных состояниях. Например, в протоколе ICMPv6 Echo узел испускает пакет ICMPv6 Echo Request и переходит в нестационарное состояние, в котором ожидает входящего пакета ICMPv6 Echo Reply. Таким образом, внешнее воздействие – пакет ICMPv6 Echo Reply – необходимо оказать в нестационарном состоянии. Для того, чтобы обойти ограничение на стационарность начального состояния, непроцедурные стимулы были специфицированы как отложенные реакции на некоторые процедурные стимулы. Мы ввели стимул “Отправить пакет IPv6 в целевую систему”. Спецификация для данного стимула тривиальна. Медиатор для данного стимула отправляет пакет IPv6 с удаленного узла. Собственно входящий пакет рассматривается как отложенная реакция на данный стимул.
Мы специфицировали два процедурных стимула:
Отправить пакет UDP Отправить ICMPv6 Echo Request
Спецификация “Отправить пакет UDP” моделирует отправку данных через UDP сокет. У данного стимула есть следующие параметры: адрес узла назначения, адрес узла отправителя (так как узел IPv6 может иметь более одного адреса), номер порта получателя и данные, которые необходимо отправить. Спецификация утверждает, что в сеть будет отправлен пакет IPv6 с заданным исходным адресом и заданным адресом назначения, который содержит пакет UDP на указанный порт и с указанными данными. Данная спецификация нацелена на проверку функции отправки пакетов в сеть. Так как точка доступа к упомянутой функции расположена глубоко внутри модуля IPv6, то для тестирования мы воспользовались функцией-посредником. В качестве посредника был выбран протокол UDP, так как UDP (в отличие от TCP) практически не обладает собственной внутренней функциональностью, и запрос на отправку пакета UDP почти точно отображается на запрос на отправку пакета IPv6. Спецификация “Отправить ICMPv6 Echo Request” моделирует протокол ICMPv6 Echo, описанный в .У данного стимула есть следующие параметры: адрес узла назначения, адрес узла отправителя (так как узел IPv6 может иметь более одного адреса) и данные, которые необходимо отправить в пакете ICMPv6 Echo Request. Спецификация утверждает, что в сеть будет отправлен пакет IPv6 с заданным исходным адресом и заданным адресом назначения, который содержит пакет ICMPv6 Echo Request с указанными данными, и что все пакеты Echo Reply, которые придут в ответ на запрос, будут доставлены в процесс, инициировавший запрос. Спецификация “Отправить ICMPv6 Echo Request” также имеет отношение к функции отправки пакетов. Но так как у данного стимула есть сложная внутренняя функциональность, не связанная с отправкой пакетов, то тестирование отправки пакетов производилось преимущественно посредством отправки пакетов UDP.
Тестовый сценарий в UniTesK определяет последовательность воздействий, которые оказываются на целевую систему. В UniTesK в качестве теоретической основы для построения тестового сценария выбрана модель конечных автоматов. Тестовый сценарий обладает собственным состоянием, которое, как правило, вычисляется на основе состояния целевой системы. В каждом состоянии задаются воздействия, которые в данном состоянии можно оказать на целевую систему. Тестовый сценарий в процессе работы обходит все состояния и в каждом состоянии оказывает все перечисленные воздействия. На рисунке 2 изображен пример тестового сценария, в котором насчитывается три состояния (S1, S2 и S3) и семь воздействий (I1_1, I1_2, I2_1, I2_2, I3_1, I3_2, I3_3). При тестировании тестовый сценарий побывает в каждом состоянии и пройдет по каждой дуге. К сожалению, для большинства целевых систем невозможно получить описание тестового сценария из спецификаций полностью автоматически, без помощи человека. Можно указать следующие причины:
Число состояний целевой системы, как правило, очень велико. Число воздействий, которые можно оказать на целевую систему в каждом состояний, как правило, очень велико.
При всем при том, число групп разных состояний, как правило, вполне обозримо. Но критерий различения состояний автоматически не определить, здесь нужна помощь человека – разработчика тестов. Число различных воздействий на целевую систему также много меньше общего числа воздействий. Из формальных спецификаций можно автоматически получить критерий различения воздействий, но автоматически построить воздействия можно только в простейших случаях. В UniTesK реализован компромиссный подход к разработке тестовых сценариев. Разработчик тестового сценария пишет процедуру различения состояний целевой системы, тем самым определяя классы эквивалентности состояний целевой системы. Каждый класс эквивалентности определяет одно состояние автомата тестового сценария. Разработчик тестового сценария также задает процедуру, которая строит всевозможные тестовые воздействия, то есть переходы автомата тестового сценария. Эти воздействия фильтруются в соответствии с одним из сгенерированных критериев покрытия. Фильтры отсеивают избыточные воздействия, то есть воздействия, которые не улучшают уже достигнутое покрытие. Фильтрация воздействий существенно упрощает написание процедур перебора воздействий. По предоставленным описаниям динамически строится граф состояний автомата тестового сценария. При обходе графа автоматически отслеживается покрытие требований, описанных в спецификациях для генерации отчета о покрытии.
В ходе проекта были разработаны 15 тестовых сценариев. Приблизительно тестовые сценарии можно разделить на 4 группы:
Тесты на отправку пакетов. Тесты из данной группы проверяют, как целевая система передает пакеты верхнего уровня в сеть. Также производится проверка того, как реализация проводит нарезку больших пакетов на фрагменты. Тесты на получение пакетов. Тесты из данной группы проверяют, как целевая система обрабатывает различные входящие пакеты. Тестируются функция сборки фрагментов и доставка пакетов протоколам верхнего уровня. Значительное место занимает проверка того, как система обрабатывает поданные на вход некорректные пакеты. Тесты для функции ICMPv6 Echo. Тесты из данной группы проверяют корректность реализации простого диагностического протокола Echo, встроенного в ICMPv6. Тесты для Neighbor Discovery. Тесты из данной группы проверяют, что реализация Neighbor Discovery соответствует требованиям, изложенным в RFC 2461 .
Заметим, что представленное разделение нестрогое, и отдельные тестовые сценарии можно отнести сразу к нескольким группам. Тестовые сценарии для MSR IPv6 осуществляют два вида тестирования:
тестовые сценарии проверяют корректность работы целевой системы на корректных входах. тестовые сценарии проверяют устойчивость целевой системы по отношению к ошибкам во входных пакетах IPv6.
В данном разделе описывается, как тестовая система оказывает воздействие на целевую систему (MSR IPv6) и собирает реакции целевой системы.
IPv6 – сетевой протокол нового поколения. Призван заменить существующий протокол сетевого уровня IPv4. IPv6 содержит ряд усовершенствований по сравнению с IPv4 и разрешает проблемы, которые ограничивают дальнейшее развитие сетей на IPv4. По эталонной модели OSI протокол IPv6 относится к протоколам сетевого уровня. На этом уровне происходит маршрутизация пакетов на основе преобразования сетевых адресов в адреса канального уровня. Сетевой уровень обеспечивает прозрачную передачу данных между транспортным уровнем и канальным уровнем.
Данный раздел содержит очень поверхностное введение в UniTesK. Более подробное описание можно найти в С 1994 года в ИСП РАН активно разрабатываются методы и инструменты тестирования программного обеспечения на основе формальных методов. В 1994-1999 годах по контрактам с Nortel Networks в ИСП РАН был разработан и активно использовался метод тестирования KVEST. KVEST отличался от обычных методов тестирования индустриального программного обеспечения тем, что в KVEST использовались формальные спецификации в форме пред- и постусловий для построения тестовых оракулов, а также модель конечных автоматов для построения тестовых воздействий. Применение KVEST показало, что формальные методы можно с большим успехом применять при тестировании индустриального программного обеспечения. Опыт применения KVEST показал, что использование академических языков формальных спецификаций и специальных языков описания тестов препятствует встраиванию инструментов, основанных на этих языках, в процесс разработки ПО. Чем ближе язык спецификаций к языку, на котором ведется разработка, тем проще разработчикам писать спецификации и тесты . UniTesK разрабатывался на основе опыта, полученного при разработке и применении KVEST. Рассмотрим основные особенности UniTesK:
Разделение построения тестовых воздействий и проверки правильности поведения целевой системы. Тестовые воздействия строятся в тестовых сценариях, а проверка правильности поведения целевой системы в тестовых оракулах. Автоматизированное построение тестовых воздействий Представление функциональных требований к целевой системе в виде формальных спецификаций Для записи формальных спецификаций используется язык, “близкий” к языку, на котором разработана целевая система Автоматическая генерация тестовых оракулов из спецификаций Оракулы и реализация связаны посредством тонкой прослойки медиаторов.
Язык описания тестовых воздействий “близок” к языку, на котором разработана целевая система Автоматически генерируются критерии качества покрытия требований Автоматически производится оценка качества покрытия требований при прогоне тестов
При тестировании мы обнаружили, что в реализации алгоритма сборки фрагментов в MSR IPv6 присутствует ошибка. При получении последовательности фрагментов определенного вида в модуле MSR IPv6 возникает исключительная ситуация, которая приводит к краху ядра операционной системы и перезагрузке Windows 2000. В MSR IPv6 некорректно спроектирован интерфейс доступа к функции ICMPv6 Echo Request. Клиентский процесс, инициировавший запрос, блокируется до прибытия первого ответа (Echo Reply) или до истечения таймаута. Если на запрос поступили ответы, то первый ответ возвращается клиенту, а все остальные отбрасываются. Такое поведение не соответствует требованию передавать клиенту все поступившие ответы . В одном частном случае реализация алгоритма сборки фрагментов в MSR IPv6 нарушает одно из требований, изложенное в RFC 2460 . RFC требует, чтобы служебная информация, которая передается во фрагментах, не попадала в восстановленный пакет. Тестирование показало, что для фрагментов определенного вида MSR IPv6 оставляет служебную информацию в восстановленном пакете. Более подробное описание выявленных дефектов можно найти в .
Медиаторы для непроцедурных стимулов
Медиаторы для процедурных стимулов
MSR IPv6 – это свободно распространяемая открытая реализация IPv6 для Windows NT/Windows 2000. Как заявляют разработчики, назначение MSR IPv6
Бесплатная общедоступная реализация IPv6 Пример реализации протокола сетевого уровня для Windows NT Исследования протоколов IPv6
В MSR IPv6 реализованы основные функции оконечного узла, описанные в предыдущем разделе, а также ряд базовых функций маршрутизаторов IPv6. Кроме того, MSR IPv6 содержит собственную реализацию транспортных протоколов TCP и UDP и интерфейс сокетов для доступа отправки и получения пакетов в сети IPv6. MSR IPv6 может устанавливаться параллельно стеку IPv4 без каких бы то ни было последствий для работоспособности последнего. Более подробную информацию о MSR IPv6 можно получить на сайте Microsoft Research и в работе .
Neighbor Discovery
Оценка покрытия кода целевой системы
Оракулы и спецификации
Рассмотрим особенности, которые отличают тестирование
Рассмотрим особенности, которые отличают тестирование MSR IPv6 от тестирования обычных программных интерфейсов. Отложенные реакции. Целевая система демонстрирует реакции, которые происходят спустя некоторое время после воздействия извне, причем это реакции нескольких видов. Непроцедурные стимулы. Целевая система допускает как процедурные, так и непроцедурные воздействия. Процедурные воздействия – вызов процедур, которые входят в программный интерфейс. Непроцедурные воздействия – входящие пакеты IPv6, которые целевая система получает из сети. Доступ к процедурным стимулам.. Реализация MSR IPv6 расположена по большей части в ядре Windows 2000, поэтому программный интерфейс MSR IPv6 напрямую не доступен. Для обращения к процедурам, которые экспортирует модуль, расположенный в ядре, необходимо пользоваться специальными средствами операционной системы. Недетерминизм реакций. Отложенные реакции, вообще говоря, недетерминированы. При одном и том же внешнем воздействии целевая система может демонстрировать различные отложенные реакции. Это связано с тем, что реакции системы определяются составляющими её внутреннего состояния, которые невозможно определить извне, а также с тем, что ряд алгоритмов в IPv6 используют случайные числа. Рассмотрим теперь, какие средства предлагает UniTesK для решения выявленных проблем. Для тестирования систем с отложенными реакциями в UniTesK разработаны методы разработки спецификаций и тестовых сценариев, основанные на формализме конечных автоматов с отложенными реакциями. Механизм медиаторов позволяет отделить модель стимулов от того, как в действительности происходит воздействие на целевую систему. С точки зрения модели не играет никакой роли, как осуществляется воздействие – вызовом процедуры, обращение к модулю ядра, отправкой пакета в целевой компьютер извне. Конкретное воздействие определяется соответствующим медиатором. В подходе UniTesK используются имплицитные спецификации. Такие спецификации описывают, какие реакции целевой системы и какие изменения в состоянии целевой системы являются допустимыми. Спецификации не вычисляют реакции и конечное состояние целевой системы, лишь проверяют условия допустимости. Это позволяет описывать недетерминизм поведения целевой системы.
Отправка и получение пакетов.
Применение UniTesK к тестированию систем с отложенными реакциями
Это накладывает ограничения на спецификации и технику тестирования. Во-первых, при разработке спецификаций используется подход “черного ящика”, при котором внутреннее состояние целевой системы недоступно и его приходится моделировать в спецификациях. Во-вторых, на целевую систему накладывается жесткое ограничение на стационарность начальных и конечных состояний. Рассмотрим последнее требование более подробно. Сериализация проводится после того, как собраны все реакции на воздействие. Это означает, что существует такой интервал времени T0, что в течение T0 с момента оказания воздействия целевая система продемонстрирует все реакции на воздействие. Состояние, в которое перейдет целевая система, обладает тем свойством, что нем система не демонстрирует спонтанных (то есть без воздействия извне) реакций. Такие состояний называются стационарными. Реализованный в UniTesK метод тестирования систем с отложенными реакциями требует, чтобы в любом состоянии конечное состояние для любого допустимого в данном состоянии воздействия было стационарным, причем существует верхняя грань времени ожидания реакций по всем состояниям и воздействиям. Кроме того, алгоритм обхода графа состояний автомата тестового сценария требует, чтобы воздействие на целевую систему оказывалось только из стационарного состояния. Несмотря на жесткость указанных ограничений, UniTesK применим для тестирования широкого класса систем с отложенными реакциями. В частности, как показал анализ документации, протокол IPv6 удовлетворяет требованию на стационарность конечных состояний, поэтому UniTesK возможно использовать для построения тестовых наборов для IPv6.
Процесс разработки тестового набора
Разбиение MSR IPvна подсистемы
Результаты
Сбор реакций целевой системы
Спецификации
Спецификации реакций
Спецификация фрагментации
Спецификация Neighbor Discovery
Спецификация непроцедурных стимулов
Спецификация процедурных стимулов
Тестовые сценарии
Транспорт стимулов и реакций
В статье представлен опыт разработки
В статье представлен опыт разработки тестового набора для реализации протокола IPv6 на Windows 2000. Тестовый набор предназначался для проверки соответствия реализации протокола IPv6 спецификациям IPv6. Проект по разработке тестового набора проходил при поддержке исследовательского гранта Microsoft Research. Разработка тестового набора проводилась с использованием методологии тестирования UniTesK, которая разработана и развивается в Институте системного программирования РАН. В качестве объекта тестирования была выбрана MSR IPv6 – реализация IPv6, разработанная в Microsoft Research. Перед тестовым набором стояла задача проверить, насколько реализация протокола соответствует стандарту протокола. Кроме того, перед разработчиками тестового набора были поставлены следующие цели:
Продемонстрировать применимость формальных методов для специфицирования и тестирования сложного API, такого как реализация IPv6 Исследовать применимость UniTesK к специфицированию и тестированию внутренних подсистем Windows NT или приложений для Windows NT Исследовать применимость UniTesK к тестированию индустриального программного обеспечения
Статья построена следующим образом. содержит краткое введение в IPv6 и описание функций IPv6, которые мы тестировали. В указаны общие сведения о MSR IPv6 и обсуждаются особенности MSR IPv6 в контексте тестирования. В дано общее описание метода разработки тестовых наборов UniTesK. посвящен применению UniTesK для тестирования систем с отложенными реакциями. В дано описание устройства тестового набора для MSR IPv6, в перечисляются результаты проекта по разработке тестового набора. – Заключение.
Введение в IPv
Введение в UniTesK
Выявленные дефекты
Проект по разработке тестового набора
Проект по разработке тестового набора для MSR IPv6 продемонстрировал применимость UniTesK для тестирования сложного API на платформе Win32. UniTesK был использован для тестирования системы, расположенной в ядре Windows 2000. Интерфейс целевой системы содержит непроцедурные стимулы и отложенные реакции. Были выявлены ошибки в системе, которая уже несколько лет находилась в эксплуатации и проходила испытания другими тестовыми наборами.
