Описание асинхронных метрик покрытия

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

Предположим, что для целевой системы были выделены k видов взаимодействий, инициируемых окружением, S = { Si | i = 1, … , k } и m видов взаимодействий, инициируемых целевой системой, R = { Rj | j = 1, … , m }. А асинхронная модель требований задана посредством асинхронной спецификации Spec = { SpecSi | i = 1, …, k; k > 0 }

{ SpecRj | j = 1, …, m; m ≥ 0 }.

Тогда метрика покрытия интерфейсной операции μ : VSi x XSi x YSi x VSi

R, являющаяся сюрьективной функцией в конечное множество R, используется для описания асинхронной метрики интерфейсной операции-стимула Si. Этой метрике покрытия соответствует асинхронная метрика покрытия асинхронной модели требований MRA[Spec], которую мы будем обозначать MA[μ].

MA[μ] = { Cr

2E | r R }, где Cr = { ( v, x, y, v' ) V x X x Y x V | μ( v, x, y, v' ) = r}.

Аналогично определяются метрики покрытия интерфейсных операций-реакций. Метрика покрытия интерфейсной операции μ : VRj x Unit x YRj x VRj

R используется для описания асинхронной метрики интерфейсной операции-реакции Rj. Этой метрике μ соответствует асинхронная метрика покрытия MA[μ] асинхронной модели требований MRA[Spec]:

MA[μ] = { Cr

2E | r R }, где Cr = { ( v, z, v' ) V x Z x V | μ( v, ε, z, v' ) = r}.

Также как и в синхронном случае, определение метрик интерфейсных операций не дает возможности задать произвольную асинхронную метрику покрытия.
Этот способ позволяет описывать только метрики покрытия, переходы которых помечены одной интерфейсной операцией. Но как показывает практический опыт, этого оказывается достаточно для измерения качества тестирования систем с асинхронным интерфейсов различных типов.
Второй способ описания метрик покрытия при помощи расширенных метрик покрытия интерфейсных операций также может быть использован при тестировании асинхронных систем. Асинхронная метрика покрытия, заданная посредством расширенной метрики покрытия интерфейсной операции Si μ' = { cp | p = 1, …, n; cp : VSi x XSi x YSi x VSi

Bool }, обозначается MA[μ']:
M[μ'] = { Cp 2E | p = 1, …, n }, где Cp = { ( v, x, y, v' ) V x X x Y x V | cp( v, x, y, v' ) }.
Также как и асинхронная метрика покрытия, заданная посредством расширенной метрики покрытия интерфейсной операции Rj μ' = { cp | p = 1, …, n; cp : VRj x Unit x YRj x VRj Bool }:
M[μ'] = { Cp 2E | p = 1, …, n }, где Cp = { ( v, z, v' ) V x Z x V | cp( v, ε, z, v' ) }.

Описание асинхронных взаимодействий в модели поведения

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

Чтобы модель поведения была согласована с моделью требований, необходимо чтобы она была построена на основе единого интерфейса целевой системы ( X, Y, Z ). Если модель требований задана спецификацией Spec, то таким образом интерфейс целевой системы ( X, Y, Z ) фиксирован согласно определению MRA[Spec]. Стимул задается интерфейсной операцией-стимулом и набором значений входных параметров этой операции, непосредственная реакция идентифицируется интерфейсной операцией-стимулом и набором значений выходных параметров этой операции, а отложенная реакция идентифицируется интерфейсной операцией-реакцией и набором значений выходных параметров этой операции.

В этом случае асинхронная модель поведения целевой системы определяется в терминах заданной спецификации. Асинхронная модель поведения состоит из набора асинхронных взаимодействий и частичного порядка над ним. Набор взаимодействий определяется посредством регистрации всех зафиксированных взаимодействий в специальном компоненте тестовой системы - регистраторе взаимодействий. А частичный порядок над этим набором задается посредством комбинации двух моделей: модели каналов и модели временных меток.

Асинхронные взаимодействия, инициированные тестовой системой, регистрируются после получения непосредственной реакции от целевой системы. Такие взаимодействия характеризуются:

идентификатором интерфейсной операции-стимула, набором значений входных параметров этой операции, набором значений выходных параметров этой операции.

Асинхронные взаимодействия, инициированные целевой системой, регистрируются после их завершения. Такие взаимодействия характеризуются:

идентификатором интерфейсной операции-реакции, набором значений выходных параметров этой операции.

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

Описание метрик покрытия

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

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

Определим способ описания метрик формально. Предположим, что в целевой системе выделено k интерфейсных операций: I = { Ii | i = 1, … , k } и требования к ее поведению были описаны в спецификации Spec = { SpecIi | i = 1, …, k }.

Тогда сюрьективная функция μ : VI x XI x YI x VI

R называется метрикой покрытия интерфейсной операции I с сигнатурой ( In, Out, Var ) , если множество R является конечным. Каждой метрике покрытия интерфейсной операции μ соответствует метрика покрытия модели требований MR[Spec], которую мы будем обозначать M[μ].

M[μ] = { Cr

2E | r R }, где Cr = { ( v, x, y, v' ) V x X x Y x V | μ( v, x, y, v' ) = r}.

Лемма.

Метрика покрытия M[μ] является управляемой тогда и только тогда, когда третий и четвертый аргументы функции μ являются несущественными.

Кроме того, в технологии UniTesK поддерживается другой вариант описания метрик покрытия. В этом варианте каждый элемент покрытия описывается предикатом, определяющим принадлежность взаимодействия через определенную интерфейсную операцию ( v, x, y, v' ) к данному элементу покрытия. Такой способ описания позволяет задавать метрики покрытия модели требований, элементы которых могут пересекаться между собой.
Но, как и в первом способе, существуют ограничения на описываемые метрики, связанные с привязкой каждой метрики только к одной интерфейсной операции.
Конечный набор предикатов μ' = { ci | i = 1, … , m; ci : VI x XI x YI x VI

Bool } называется расширенной метрикой покрытия интерфейсной операции I с сигнатурой ( In, Out, Var ). Каждой расширенной метрике покрытия интерфейсной операции μ' соответствует метрика покрытия модели требований MR[Spec], которую мы будем обозначать M[μ'].
M[μ'] = { Ci 2E | i = 1, … , m }, где Ci = { ( v, x, y, v' ) V x X x Y x V | ci( v, x, y, v' ) }.
Лемма.
Метрика покрытия M[μ'] является управляемой тогда и только тогда, когда третий и четвертый аргументы всех предикатов ci являются несущественными.

Описание модели поведения

Требования к функциональности целевой системы являются исходными данными для процесса тестирования. Соответственно, модель требований к целевой системе описывается во время разработки теста и в процессе тестирования не изменяется.

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

Так как модель поведения используется для сравнения с моделью требований, то эти модели должны быть согласованы между собой. Это означает, что обе модели должны быть построены на основе единого интерфейса целевой системы ( X, Y, V ).

Если модель требований задана спецификацией Spec, то таким образом интерфейс целевой системы ( X, Y, V ) фиксирован согласно определению MR[Spec]. Состояние системы определяется значениями переменных состояния, описанных в спецификации, стимул задается интерфейсной операцией и набором значений входных параметров этой операции, а реакция идентифицируется интерфейсной операцией и набором значений выходных параметров этой операции.

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

набором значений переменных до вызова интерфейсной функции; идентификатором интерфейсной операции и набором значений входных параметров этой операции; идентификатором интерфейсной операции и набором значений выходных параметров этой операции; набором значений переменных после вызова интерфейсной функции.

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

Описание модели требований

Рассмотрим подход программных контрактов более детально и определим способ описания модели требований, применяемый в технологии UniTesK. Сигнатурой интерфейсной операции I называется тройка ( In, Out, Var ), где

In = { xi | i = 1, …, in(I) ; in(I) ≥ 0 } - упорядоченный набор входных параметров операции, Out = { yi | i = 1, …, out(I) ; out(I) ≥ 0 } - упорядоченный набор выходных параметров операции, Var = { vi | i = 1, …, var(I) ; var(I) ≥ 0 } - набор переменных состояния, к которым обращается данная операция.

Каждый входной параметр xi может принимать значения из непустого множества допустимых значений Xi, каждый выходной параметр yi может принимать значения из непустого множества допустимых значений Yi, а каждая переменная состояния vi может принимать значения из непустого множества допустимых значений Vi. Эти непустые множества допустимых значений далее будут называться типами параметров и переменных.

Рассмотрим пример операции вычисления квадратного корня. Сигнатурой этой операции является тройка ( { x1 }, { y1 }, {} ). Множеством допустимых значений единственного входного параметра x1 и единственного выходного параметра y1 является множество действительных чисел R. Пустое множество переменных состояния означает, что данная операция никак не зависит ни от одной переменной состояния.

Введем следующие обозначения:

XI = X1 x … x Xin(I), если in(I) > 0, и XI = { ε }, в противном случае;

YI = Y1 x … x Yout(I), если out(I) > 0, и YI = { ε }, в противном случае;

VI = V1 x … x Vvar(I), если var(I) > 0, и VI = { ε }, в противном случае.

Спецификацией интерфейсной операции I с сигнатурой ( In, Out, Var ) называется пара предикатов ( preI, postI ), в которой

preI - предикат на множестве VI x XI, называемый предусловием, postI - предикат на множестве VI x XI x YI x VI, называемый постусловием.

Спецификация интерфейсной операции утверждает, что если презначения переменных состояния и значения входных параметров удовлетворяют предусловию, то значения выходных параметров и постзначения переменных состояния должны удовлетворять постусловию для данных презначений переменных состояния и значений входных параметров.
Например, спецификацию операции вычисления квадратного корня ( presqrt, postsqrt ) можно задать следующим образом:
presqrt ( v, x1 ) ≡ (x1 ≥ 0)
postsqrt ( v, x1, y1, v' ) ≡ &#x007C; x1 - y12 &#x007C; < εпогр
Здесь, как и ранее, εпогр обозначает некоторое положительное действительное число.
Спецификацией целевой системы называется непустой набор спецификаций ее интерфейсных операций &#x007B; SpecIi &#x007C; i = 1, …, k; k > 0 &#x007D;.
В технологии UniTesK для описания требований к функциональности целевой системы (модели требований) также используется подход программных контрактов. Описание модели требований задается в виде спецификации Spec &#x007B; SpecIi &#x007C; i = 1, …, k &#x007D;, а соответствующая ей модель требований MR[Spec] ( V, X, Y, E ) определяется согласно следующим правилам:
Если в спецификации присутствует хотя бы одна переменная состояния, то множество состояний V является декартовым произведением множеств допустимых значений всех переменных состояния
V=,

где VarSpec является объединением переменных состояния всех интерфейсных операций, принадлежащих спецификации
VarSpec = .
Если в спецификации не участвует ни одной переменной состояния, то множество состояний состоит из единственного элемента ε:
V &#x007B; ε &#x007D;.
Множество стимулов X является дизъюнктивным объединением декартовых произведений множеств допустимых значений входных параметров всех интерфейсных операций спецификации
X = .
Мы будем считать, что каждый элемент дизъюнктивного объединения помечается именем интерфейсной операции и таким образом эти элементы не пересекаются между собой.


Множество реакций Y является дизъюнктивным объединением декартовых произведений множеств допустимых значений выходных параметров всех интерфейсных операций спецификации
Y = .
Мы будем считать, что каждый элемент дизъюнктивного объединения помечается именем интерфейсной операции и таким образом эти элементы не пересекаются между собой.
Множество переходов E состоит из всех переходов, удовлетворяющих обобщенным предусловию и постусловию спецификации
E = &#x007B; ( v, x, y, v' ) V x X x Y x V &#x007C; pre( v, x ) post( v, x, y, v' ) &#x007D;,

где предикат pre = , а предикат post =

Опыт применения технологии UniTesK для тестирования систем с асинхронным интерфейсом

В данной главе мы рассмотрим опыт применения технологии UniTesK для тестирования систем с асинхронным интерфейсом. Рассмотренный метод и его реализация в системе тестирования CTesK использовались в шести проектах по тестированию различного программного обеспечения, проводившихся в Институте Системного Программирования РАН.

Основные понятия

Перед началом рассмотрения технологии UniTesK введем несколько базовых терминов.

Целевой системой будем называть программную систему, которую необходимо протестировать. В качестве синонима целевой системы также будем использовать словосочетание тестируемая система. В англоязычной литературе этим терминам соответствуют сокращения SUT (System Under Test) и IUT (Implementation Under Test).

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

Параллельные воздействия на целевую систему

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

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

параллельная работа независимых тестовых сценариев; параллельное выполнение сценарных функций в рамках работы одного тестового сценария; организация параллельных воздействий на уровне сценарных функций.

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

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

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

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

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

Прикладные бинарные интерфейсы ОС Linux

Еще одним крупным проектом, в рамках которого метод спецификации и тестирования систем с асинхронным интерфейсом играет существенную роль, является проект по формализации требований стандартов и разработки автоматизированного тестового набора для бинарных интерфейсов операционной системы Linux, проводимый в рамках проекта по созданию Центра верификации ОС Linux [].

В этом проекте предполагается формализация требований к 1532 функциям прикладного бинарного интерфейса ОС Linux, описанным в стандарте Linux Standard Base Core 3.1 []. Данные функции были сгруппированы по двухуровневой схеме, согласно реализуемой ими функциональности. На верхнем уровне функции были распределены по кластерам, а кластеры были разбиты на подсистемы. Кроме того, если размеры подсистемы оказывались достаточно большими и входящие в нее функции логически разделялись на несколько групп, подсистема разбивалась на группы функций. Список всех подсистем и групп функций, описанных в Linux Standard Base Core 3.1, представлен на сайте проекта [].

Для каждой группы функций проведен анализ потребности в применении метода асинхронного тестирования. Из 137 групп функций только 50 групп (36&#x0025;) могут быть полностью протестированы синхронным образом. Для полного описания требований к 13 группам функций (9&#x0025;) необходимо использовать асинхронные реакции. 18 групп функций (13&#x0025;) содержат блокирующиеся функции, а для тестирования 56 групп функций (42&#x0025;) требуется одновременное участие целевой системы в нескольких взаимодействиях со своим окружением.

Процесс тестирования в технологии UniTesK

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

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

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

выделение и анализ ошибочного поведения целевой системы и тестового набора; оценка качества тестирования и анализ тестового покрытия.

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

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

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

Поэтому на этапе анализа результатов тестирования используются общие инструменты анализа результатов выполнения тестового набора, построенного по технологии UniTesK. Таких инструментов два. Генератор статических отчетов создает статистические отчеты в формате HTML. Эти отчеты содержат информацию о достигнутом покрытии метрик покрытия, графе автоматного тестового сценария и найденных несоответствиях между поведением реализации и моделью требований. Динамический анализатор трассы позволяет пользователю анализировать результаты тестирования в интерактивном режиме, предоставляя различные представления трассы (граф тестового сценария, MSC диаграмма [], структурированное представление).

Проекция технологии UniTesK на язык программирования C

Процесс тестирования по технологии UniTesK на платформе языка программирования C поддерживается семейством инструментов CTesK. Работа семейства инструментов CTesK устроена по принципам, рассмотренным в предыдущем разделе.

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

спецификационные типы; подтипы (инварианты типов); инварианты переменных; спецификационные функции; медиаторные функции; сценарные функции; тестовые сценарии.

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

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

Спецификационные функции предназначены для описания модели требований. Каждая спецификационная функция определяет спецификацию одной интерфейсной операции. Спецификационная функция состоит из сигнатуры и тела.

Сигнатура спецификационной функции задает сигнатуру, соответствующей интерфейсной операции. Параметры спецификационной функции и их типы описываются как параметры обычной функции языка C. Для описания набора переменных модельного состояния, с которыми работает данная функция, используется дополнительная конструкция языка SEC, получившая название ограничения доступа. Ограничение доступа содержит список переменных модельного состояния с указанием вида доступа, осуществляемого к каждой переменной.
Набор метрик покрытия описывается последовательностью составных операторов, помеченных ключевым словом SEC coverage и идентификатором покрытия. Код внутри каждого отдельного составного оператора эквивалентен коду функции языка C, имеющей те же параметры, что и спецификационная функция, и возвращающей значение перечислимого типа. Этот перечислимый тип не определяется явным образом, а получается объединением всех идентификаторов, использованных в операторах return внутри данного составного оператора. Таким образом, составной оператор определяет метрику покрытия интерфейсной операции, а идентификатор покрытия задает имя этой метрики.

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

Для задания модели поведения целевой системы используется другой вид функций SEC, называемых медиаторными. Каждой медиаторной функции соответствует некоторая спецификационная функция, которая получила название базовой спецификационной функции. Сигнатура медиаторной функции состоит из ключевого слова SEC mediator, идентификатора медиаторной функции, ключевого слова for и сигнатуры базовой спецификационной функции. Тело медиаторной функции представляет собой тело функции языка C, имеющей те же параметры и тот же тип возвращаемого значения, что и базовая спецификационная функция.

Медиаторная функция должна выполнить следующую последовательность действий:

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

Каждое выполнение медиаторной функции в процессе тестирования рассматривается как выполнение одного взаимодействия между тестовой системой и целевой системой.


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

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

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

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

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

библиотека абстрактных типов данных; библиотека поддержки тестовой системы; библиотека поддержки времени исполнения SEC; библиотека функций трассировки событий.

Программные контракты

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

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

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

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

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

Протокол MPEG-2 IPMP

Еще одним примером применения технологии UniTesK для тестирования телекоммуникационных протоколов был пилотный проект по тестированию реализации протокола MPEG-2 IPMP, выполненный ИСП РАН совместно с Morphibius Technology Inc., Канада.

Основной целью данного проекта являлся анализ возможностей использования тестирования на соответствие стандарту для обеспечения корректности взаимодействия между различными реализациями этого стандарта. Одним из направлений работ по проекту стала разработка формальных спецификаций и тестового набора для нескольких важных вариантов использования MPEG-2 IPMP:

обработка управляющей информации протокола IPMP; работа с IPMP дескрипторами; обработка потока данных IPMP.

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

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

Впервые рассматриваемый подход использовался для

Впервые рассматриваемый подход использовался для тестирования реализации протокола IPv6 от Microsoft Research, которое проводилось в рамках совместного проекта ИСП РАН и Microsoft Research, Cambridge [, ].

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

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

Требования к поведению тестируемой системы извлекались из 10 RFC (RFC 2460, RFC 2461, RFC 2462, RFC 2463, RFC 2464, RFC 3513, RFC 2373, RFC 2292, RFC 2553 и RFC 2675). После изучения этих требований происходила их формализация в виде предусловий и постусловий интерфейсных операций, моделирующих взаимодействия с тестируемой системой.

Тестирование проводилось при помощи 15 стационарных асинхронных тестовых сценариев, которые эмулировали различные варианты использования функций протокола IPv6 на основе обхода детерминированных графов. Эти сценарии позволили обнаружить 4 ошибки в целевой системе, 2 из которых являлись фатальными и приводили к перезагрузке системы при получении определенной последовательности пакетов IPv6. Такая последовательность пакетов может быть использована для организации атаки типа "Отказ в обслуживании".

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

Результаты апробации

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

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

участие тестируемой системы в нескольких одновременных взаимодействиях с окружением; блокируемые вызовы функций; получение асинхронных реакций от целевой системы.

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

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

Результаты главы

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

Сценарные функции

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

Сценарной функцией для целевой системы с интерфейсом ( X, Y, V ) называется шестерка ( GS, PS, IS, C, is0, π ), где:

GS - множество внешних состояний; PS - множество параметризующих состояний; IS - множество внутренних состояний; C = ( CS, A, B, E, Q ) - управляющий автомат, в котором: CS = GS x PS x IS - состояние автомата состоит из декартова произведения всех видов состояний сценарной функции, A = X

V, B = (Y x V) &#x007B; ε &#x007D;, E CS x A x B x CS, Q CS; is0 : V x GS IS - функция инициализации сценарной функции; π : V x GS (PS) - функция, определяющая множество параметризующих состояний для данных внешнего состояния и состояния целевой системы. Это множество мы будем называть множеством параметров.

Множество всех сценарных функций для целевой системы с интерфейсом ( X, Y, V ) и имеющее множество внешних состояний GS мы будем обозначать Σ( X, Y, V, GS ).

Автоматным тестовым сценарием со сценарными функциями для целевой системы с интерфейсом ( X, Y, V ) называется шестерка ( GS, gs0, VG, vg, α,

), где:

GS - множество глобальных состояний сценария; gs0 : V

GS - функция инициализации глобального состояния; VG - множество вершин графа автомата; vg : V x GS VG - функция вычисления вершины графа сценария; α - неизбыточный алгоритм движения по графу сценария, - конечный набор сценарных функций Σi Σ( X, Y, V, GS ).

Множества параметров всех сценарных функций должны быть согласованы с вершинами графа сценария:

i &#x007B; 1, …, k &#x007D; v1,v2 V gs1,gs2 GS

vg( v1, gs1 ) = vg( v2, gs2 )

πΣi( v1, gs1 ) = πΣi( v2, gs2 ).

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

Исходя из этого ограничения, можно определить множество параметров сценарной функции Σi в данной вершине графа vg как:

πΣi( v, gs ), если v V gs GS : vg( v, gs ) = vg; &#x007B;&#x007D;, иначе.

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

Автоматным механизмом сценарных функций называется функция, преобразующая автоматный тестовый сценарий со сценарными функциями ( GS, gs0, VG, vg, α, ) в тестовый сценарий, посредством применения автоматного механизма построения тестового сценария к автоматному тестовому сценарию ( IG', vg0', α', S', ρ', &#x03b3;', &#x03b7;' ), определенному по следующим правилам:

неизбыточное описание ориентированного графа IG' = ( VG', XG', π' ) состоит из:

множества вершин, совпадающего с множеством вершин графа автомата VG (VG' = VG), множества стимулов, являющегося дизъюнктивным объединением параметризующих состояний всех сценарных функций (XG' = ), функции, определяющей множество допустимых стимулов π' = ;

функция инициализации графа сценария vg0': vg0'(v) ≡ vg( v, gs0(v) ); неизбыточный алгоритм α' = α; множество состояний сценария S' = GS x V x State,
где State = &#x007B;ε&#x007D;; функция рестарта сценария ρ': ρ'( (gs,v,state) ) ≡ ( gs, v, ε ); сценарное воздействие &#x03b3;'( vg, psi ) = ( ( S', A', B', E', Q' ), s'0 ) ( X, Y, V, S' ) определяется для каждой пары ( vg, psi ) следующим образом:

A' = X V, B' = (Y x V) &#x007B; ε &#x007D;, E' = &#x007B; ( ( gs, v, state ), a, b, ( gs', ( ps'i, v', is'i) ) ) :

( ( state = ε )

( ( gs, psi, isi,0( v, gs ) ), a, b, ( gs', ps'i, is'i ) ) Ei


)

( ( isi ISi state = ( psi, isi) )

( ( gs, psi, isi ), a, b, ( gs', ps'i, is'i ) ) Ei
)

( a V ) v' = a

( b = ( yb, vb ) Y x V ) v' = vb &#x007D;,

Q' = &#x007B; ( gs, v, state ) S' :
( ( state = ε )
( gs, psi, isi,0( v, gs ) ) Qi
)

( ( isi ISi state = ( psi, isi) ) ( gs, psi, isi ) Qi
)
&#x007D;, s'0(v0) = ( gs0(v0), v0, ε );

отображение &#x03b7;'( vg1, psi, v, ( gs, v2, state ) ) = vg( v, gs ).

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

Системы с асинхронным интерфейсом

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

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

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

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

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

Основополагающим камнем в математических моделях технологии UniTesK являются понятия взаимодействия и модели поведения целевой системы. Именно в этих терминах описывается процесс тестирования и на их основе строятся все остальные модели.

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

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

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

Рисунок 10. Стек протоколов

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

Спецификация и тестирование систем с асинхронным интерфейсом

Институт системного программирования

Российской академии наук

Аннотация.

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

,

Институт системного программирования

Российской академии наук

Стационарное тестирование асинхронных систем

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

В большинстве случаев одного теста такого размера оказывается недостаточно для достижения требуемого качества тестирования. Как следствие, появляется необходимость в построении набора тестов небольшого размера. Если разрабатывать такие наборы тестов независимо друг от друга, то при этом теряется одно из основных достоинств технологии UniTesK - автоматическое построении сложных последовательностей тестовых воздействий.

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

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

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

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

)] асинхронной модели поведения ( P, ) будем называть асинхронную модель поведения ( P', ' ), в которой:

P' = P &#x007B;(done,ε)&#x007D;, ' = &#x007B; ( p, (done,ε) ) &#x007C; p P &#x007D;.

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

Стабилизирующие трансформации обоих моделей единообразно модифицируют асинхронный интерфейс целевой системы, добавляя в него псевдостимул done и непосредственную реакцию ε. Таким образом, если исходные модели были построены для общего асинхронного интерфейса ( X, Y, Z ), то их стабилизирующие трансформации будут для общего асинхронного интерфейса ( X &#x007B;done&#x007D;, Y &#x007B;ε&#x007D;, Z ).

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

Входными данными для алгоритма проверки корректности поведения являются конечная асинхронная модель поведения целевой системы ( P, ) и асинхронная модель требований A = ( V, X, Y, Z, E ) с начальным состоянием v0 V.

Стационарный автоматный тестовый сценарий

Рассмотрим реализацию предложенного подхода более формально.

Стационарным автоматным тестовым сценарием относительно асинхронной модели требований A = ( V, X, Y, Z, E ) с множеством стабильных состояний VS

V и начальным состоянием v0 VS, называется пятерка ( SA, ASt, AIR, AHO, AGS ), где

SA = ( DA, Afsm, VG, XG, vg0, α,

) - асинхронный автоматный тестовый сценарий со сценарными функциями для целевой системы с асинхронным интерфейсом ( X, Y, Z ), ASt = ( SSt, s0,St, XSt, YSt, ESt, QSt ) - выделенный взаимодействующий автомат, входящий в состав DA, и называемый стабилизирующим автоматом асинхронного тестового сценария DA, AIR Ã( Unit, ( Ω(X,Y,Z) ) ) - асинхронная функция, замыкание которой по множеству &#x007B; stop, abort &#x007D; входит в состав DA, AHO Ã( ( Ω(X,Y,Z) ) x V, Bool x V ) - асинхронная функция, замыкание которой по множеству &#x007B; stop, abort &#x007D; входит в состав DA, AGS Ã( Unit, VG ) - асинхронная функция, замыкание которой по множеству &#x007B; stop, abort &#x007D; входит в состав DA;

и для которой выполнены следующие ограничения:

вхождения замыканий взаимодействующих автоматов AIR, AHO и AGS и вхождения ASt, Afsm и Σi в DA различаются между собой, SSt = ( &#x007B; s0, s1, s2, s4, s5, s6, final &#x007D;

Ω(X,Y,Z) ) x V, s0,St = ( s0, v0 ), XSt = &#x007B; callIR, callGS, abort &#x007D; &#x007B; callHO,P,v &#x007C; P Ω(X,Y,Z), v V &#x007D;, YSt = &#x007B; stop, abort &#x007D; &#x007B; resultHO,verdict,v &#x007C; verdict Bool, v V &#x007D;

&#x007B; resultIR,P &#x007C; P Ω(X,Y,Z) &#x007D;,

где RXi = &#x007B; resulti,true, resulti,false &#x007D;, ESt = &#x007B; ( ( s0, v ) resulti,true?, ( s1, v ) ) &#x007C; i = 1, …, k &#x007D;

&#x007B; ( ( s1, v ), callIR!, ( s2, v ) ) &#x007D;

&#x007B; ( ( s2, v ), resultIR,P?, ( P, v ) ) &#x007C; P Ω(X,Y,Z) &#x007D;


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

Работа по оценке корректности модели поведения выполняется в асинхронной функции AHO, которая получает на вход текущее состояние модели требований и асинхронную модель поведения. К модели поведения применяется стабилизирующая трансформация и затем проверяется корректность этой трансформации относительно стабилизирующей трансформации модели требований ST[A,VS] с начальным состоянием, равным текущему состоянию модели требований. В дополнение к оценке корректности AHO возвращает основную составляющую конечного состояния линеаризации, которая становится новым текущим состоянием модели требований.

Однако, конечное состояние линеаризации может быть найдено только в том случае, когда все успешные линеаризации модели поведения ST[P] завершаются в одном и том же состоянии. Если это условие не выполняется, то асинхронная функция AHO не может выполнить свою задачу и, соответственно, стационарный автоматный тестовый сценарий не может быть применен.

Далее, мы обратимся к вопросу применимости стационарного автоматного тестового сценария и определим достаточные условия для его корректной работы.

Асинхронная модель требований A = ( V, X, Y, Z, E ) называется стационарно-детерминированной относительно множества стабильных состояний VS V, если для любого конечного мультимножества асинхронных взаимодействий P и для любого состояния v VS



Лемма.

Если асинхронная модель требований A = ( V, X, Y, Z, E ) является стационарно-детерминированной относительно множества стабильных состояний VS V, то произвольный стационарный автоматный тестовый сценарий относительно модели требований A с множеством стабильных состояний VS и начальным состоянием v0 VS применим независимо от поведения целевой системы.



То есть v' VS, что и требовалось доказать.

2. В качестве завершающего шага мы докажем, что для любой асинхронной модели поведения P, если стабилизирующая трансформация этой модели ST[P] удовлетворяет стабилизирующей трансформации ST[A,VS] с начальным состоянием (v,T), где v стабильно (v VS), то конечное состояние линеаризации (v',x') существует. Из этого следует, что асинхронная функция AHO всегда может выполнить свою задачу, так как согласно первому пункту она всегда получает на вход только стабильные состояния модели требований.

Предположим, что это не так. То есть существует асинхронная модель поведения P, стабильное состояние модели требований v VS и два состояния (v',x') и (v'',x'') такие, что

&#x007B; (v',x'), (v'',x'') &#x007D; и (v',x') ≠ (v'',x'').

Тогда существует две линеаризации модели поведения ST[P] ( p1,1, p1,2, …, p1,n ) и ( p2,1, p2,2, …, p2,n ) такие, что

(v', x') ( (v,T), ( p1,1, p1,2, …, p1,n ) ) и

(v'',x'') ( (v,T), ( p2,1, p2,2, …, p2,n ) ).

Повторяя рассуждения из первого пункта, можно показать, что x' = x'' = T, p1,n = p2,n = (done,ε), v' VS, v'' VS и

(v', F) ( (v,T), ( p1,1, p1,2, …, p1,n-1 ) ) и

(v'',F) ( (v,T), ( p2,1, p2,2, …, p2,n-1 ) ).

То есть в асинхронной модели требований ST[A,VS] существует путь, начинающийся в (v,T), помеченный ( p1,1, p1,2, …, p1,n-1 ) и заканчивающийся в (v', F):

(v,T) (v2,x2) … (v', F).

Так как &#x007B; p1,1, p1,2, …, p1,n-1 &#x007D; ( (X x Y) Z ), то из определения ST[A,VS] следует, что в исходной модели требований A существует путь

v v2 … v'.

Следовательно, v' ( v, ( p1,1, p1,2, …, p1,n-1 ) ).

Аналогично, v'' ( v, ( p2,1, p2,2, …, p2,n-1 ) ).

И так как мультимножества взаимодействий &#x007B; p1,1, p1,2, …, p1,n-1 &#x007D; и &#x007B; p2,1, p2,2, …, p2,n-1 &#x007D; совпадают, то существует мультимножество взаимодействий P* = &#x007B; p1,1, p1,2, …, p1,n 1 &#x007D;:

&#x007B; v', v'' &#x007D; , причем v' ≠ v'' и v' VS, v'' VS.

То есть



Предположим также, что в процессе работы стационарного автоматного тестового сценария ( SA, ASt, AIR, AHO, AGS ) относительно модели требований A с множеством стабильных состояний VS и начальным состоянием v0 VS асинхронная функция AIR последовательно возвращала стабилизирующему автомату асинхронные модели поведения . Тогда, все вердикты функции AHO, посланные стабилизирующему автомату, были положительными, в том, и только в том случае, когда последовательная композиция стабилизирующих трансформаций моделей поведения удовлетворяет стабилизирующей трансформации модели требований ST[A] с начальным состоянием v0.

Доказательство.

1. Докажем утверждение леммы в прямую сторону. Предположим, что все вердикты функции AHO, посланные стабилизирующему автомату, были положительными, и покажем, что последовательная композиция удовлетворяет ST[A] с начальным состоянием v0.

В пункте 2 предыдущей леммы мы показали, что если асинхронная функция AHO получает на вход асинхронную модель поведения Pi и состояние модели требований v и возвращает положительный вердикт и конечное состояние линеаризации v', то в модели требований ST[A] существует путь (v,T) … (v',F) (v',T) для некоторой линеаризации ( pi,1, pi,2, …, pi,n(i)-1, pi,n(i) ) модели ST[Pi] и pi,n (i) = done.

Как мы уже отмечали, функция AHO получает на вход состояние модели требований, которое хранится в стабилизирующем автомате сценария. Это состояние инициализируется в начале работы сценария начальным состоянием v0, а в дальнейшем оно изменяется только в переходах вида ( ( s4, v ), resultHO,true,v'?, ( s5, v' ) ). Эти переходы осуществляются при получении результата от асинхронной функции AHO, так как согласно четырнадцатому ограничению стационарного автоматного тестового сценария каждой реакции получения результата асинхронной функции AHO из стабилизирующего автомата resultHO,true,v' соответствует единственный в рамках DA стимул, принадлежащий соответствующей асинхронной функции.

Отсюда следует, что в модели требований ST[A] существует путь



где ( p1,1, …, p1,n(1)-1, p1,n(1) , p2,1, …, p2,n(2)-1, p2,n(2) , …, pk,1, …, pk,n(k)-1, pk,n(k) ) - некоторая линеаризацией последовательной композиции . Согласно определению стабилизирующей трансформации максимальным элементом в SP[ (Pi,i) ] является псевдовзаимодействие (done,ε). Следовательно i &#x007B;1,…,k&#x007D; pi,n(i) = (done,ε).

По определению стабилизирующей трансформации модели требований ST[A] все переходы, помеченные (done,ε), имеют вид ( (w,F), (done,ε), (w,T) ), где w VS. То есть

i &#x007B;1,…,k&#x007D; (vi,n(1)-1, xi,n(i)-1) (vi,n(i) , xi,n(i) ) ≡ (v'i,F) (v'i,T),

где v'i VS.

Докажем по индукции, что i &#x007B;1, …, k-1&#x007D; в результате i-го вызова функции AHO из стабилизирующего автомата, та возвращает состояние модели требований равное v'i.

База индукции . Согласно определению стабилизирующего автомата функция AHO в первый раз получает модель поведения (P1,1) и состояние v0 VS. Если k > 1, то функция возвращает положительный вердикт и основную составляющую конечного состояния линеаризации ( v', x' ). Так как модель требований A является стационарно-детерминированной, то конечное состояние линеаризации существует, причем v' = v'1, так как (v0,T) … (v'1,F) (v'1,T) является успешной линеаризацией модели (P1,1).

Предположение индукции . Предположим, что после i-го вызова функции AHO из стабилизирующего автомата, та возвращает состояние модели требований v'i.

Шаг индукции . Докажем, что если после i+1-го вызова функция AHO возвращает положительный вердикт и состояние модели требований w, то w = v'i+1.

По определению стабилизирующего автомата при i+1-ом вызове функция AHO получает модель поведения (Pi+1,i+1) и состояние v'i VS. Если i+1 < k, то по условиям леммы функция возвращает положительный вердикт и основную составляющую конечного состояния линеаризации w. Заметим, что в автомате ST[A] существует путь (v'i,T) … (v'i+1,F) (v'i+1,T), который является одной из успешных линеаризаций модели (Pi+1,i+1).

Технология UniTesK

Комплексный подход, позволяющий автоматизировать целый спектр задач тестирования на основе математических моделей, представляет собой технология тестирования UniTesK [, , ], разработанная в Институте Системного Программирования РАН. Данная технология использует широко известный подход программных контрактов [] для формального описания требований к программному обеспечению и уникальные методы генерации сложных последовательностей тестовых воздействий на основе неявного описания конечного автомата. Эффективность такого подхода была подтверждена в многочисленных проектах [], и, в частности, при разработке тестового набора для ядра операционной системы канадского телекоммуникационного гиганта Nortel Networks [].

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

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

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

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

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



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

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

Таким образом, технология UniTesK не предоставляет замену методам доказательства корректности программ, но позволяет воспользоваться формальным математическим базисом для разработки качественных тестов с меньшим уровнем затрат по сравнению с обычными методами разработки тестов.

Тестирование с открытым стационарным состоянием

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

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

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

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

Тестирование систем с асинхронным интерфейсом, при котором тестовая система получает достоверную информацию о внутреннем состоянии целевой системы, во время нахождения той в стационарном состоянии, называется тестированием с открытым стационарным состоянием.

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

Тестирование систем с асинхронным интерфейсом

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

Тестирование систем с асинхронным интерфейсом на платформе языка C

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

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

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

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

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

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

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

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


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

На пятом шаге разрабатываются тестовые сценарии. Чтобы определить тестовый сценарий в SEC необходимо указать механизм построения тестового сценария и исходные данные, необходимые для этого механизма. Для систем с синхронным интерфейсом в системе тестирования CTesK реализован единственный механизм построения тестовых сценариев - механизм dfsm. В качестве исходных данных механизма dfsm выступают

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

Для поддержки асинхронного стационарного тестирования в набор исходных данных для механизма dfsm были добавлены три дополнительных элемента:

функция сохранения модельного состояния; функция восстановления модельного состояния; функция проверки стационарности текущего модельного состояния.

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

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

Тестовый сценарий

Тестом целевой системы с интерфейсом ( X, Y, V ) называется конечная или бесконечная последовательность взаимодействий &#x007B; ( vi, xi, yi, v'i ) &#x007D;. Множество всех тестов целевой системы с интерфейсом ( X, Y, V ) будем обозначать символом ℵ( X, Y, V ).

Моделью поведения целевой системы в ходе теста &#x007B; ( vi, xi, yi, v'i ) &#x007D; будем называть мультимножество взаимодействий &#x007B; ( vi, xi, yi, v'i ) &#x007D;.

Тест &#x007B; ( vi, xi, yi, v'i ) &#x007D; целевой системы с интерфейсом ( X, Y, V ) будем называть успешным относительно модели требований A = ( V, X, Y, E ), если модель поведения в ходе теста удовлетворяет модели требований A. В противном случае, тест будет называться неуспешным.

Определение 4.

Тестовым сценарием для целевой системы с интерфейсом ( X, Y, V ) называется пара ( C, s0 ), где

C - управляющий автомат ( S, A, B, E, Q ), в котором множество стимулов A = X

V, множество реакций B = (Y x V) &#x007B; ε &#x007D;, множество переходов включает в себя только переходы ( s, a, b, s' ), в которых либо a X и b (Y x V), либо a V и b = ε; s0 : V S - функция инициализации.

Тестовый сценарий управляет процессом тестирования, выполняя одно из двух возможных действий: либо подавая стимул x

X, либо устанавливая новое состояние v V. Реакцией на первое действие является реакция целевой системы y и ее постсостояние v', а на второе - пустая реакция ε. Функция инициализации определяет начальное состояние управляющего автомата в зависимости от начального состояния целевой системы.

Множество всех тестовых сценариев для целевой системы с интерфейсом ( X, Y, V ) будем обозначать символом

( X, Y, V ). Множество тестовых сценариев для целевой системы с интерфейсом ( X, Y, V ) и с заданным множеством состояний управляющего автомата S будет обозначаться ( X, Y, V, S ).

Пусть &#x007B; ej = ( sj, aj, bj, s'j ) &#x007D; является функционированием тестового сценария σ для целевой системы с интерфейсом ( X, Y, V ).
Тогда &#x007B; ek(i) = ( sk(i), ak(i), bk(i), s'k(i) ) &#x007D; будем обозначать подпоследовательность последовательности &#x007B; ej &#x007D; составленную из переходов, действия которых связаны с подачей стимула ( ak(i)

X ).

Результатом применения тестового сценария σ = ( C = ( S, A, B, E, Q ), s0 ) к целевой системе, находящейся в начальном состоянии v0 V, является тест &#x007B; ( vi, xi, yi, v'i ) &#x007D;, для которого существует такое функционирование управляющего автомата C с начальным состоянием s0(v0) &#x007B; ej = ( sj, aj, bj, s'j ) &#x007D;, что длина теста совпадает с длиной подпоследовательности &#x007B; ek(i) &#x007D; и для каждого взаимодействия ( vi, xi, yi, v'i ) выполнены следующие условия:

пресостояние vi совпадает с начальным состоянием целевой системы v0, если k(i) = 1; ранее установленным состоянием ak(i)-1, если k(i) > 1 и ak (i)-1 V; постсостоянием после предыдущей подачи стимула vi-1, если k(i) > 1 и ak(i)-1 X; стимул xi совпадает с ak(i); реакция yi совпадает с первым элементом реакции bk(i) = ( yk(i), vk(i) ); постсостояние v'i совпадает со вторым элементом реакции bk(i) = ( yk(i), vk(i) ).

Такой тест мы будем обозначать T( σ, v0 ).

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

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

Тестовым сценарием с внутренними переходами для целевой системы с интерфейсом ( X, Y, V ) называется пара ( C, s0 ), где

C - управляющий автомат ( S, A, B, E, Q ), в котором множество стимулов A X V &#x007B; ε &#x007D;, множество реакций B (Y x V) &#x007B; ε &#x007D;, множество переходов включает в себя только переходы ( s, a, b, s' ), в которых либо a X и b (Y x V), либо a V &#x007B; ε &#x007D; и b = ε; s0 : V S - функция инициализации.



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

Каждому тестовому сценарию с внутренними переходами σε = ( ( S, A, B, E, Q ), s0 ) соответствует тестовый сценарий σ( σε ) = ( ( S, A', B, E', Q' ), s0 ), в котором

множество стимулов A' = X V, множество переходов E' состоит из переходов ( s, a, b, s' ) S x A' x B x S, для которых существует путь s1 s2 … sn в управляющем автомате ( S, A, B, E, Q ), удовлетворяющий следующим условиям: начальное состояние пути s1 = s, конечное состояние пути sn = s', i &#x007B; 1, …, n-1 &#x007D;: (ai = a) (bi = b)
j &#x007B; 1, …, n-1 &#x007D; (i ≠ j) (aj = ε) (bj = ε); множество заключительных состояний Q' состоит из состояний множества Q, а также из состояний s S, из которых не выходит ни одного перехода во множестве E', но существует путь s1 s2 … sn в управляющем автомате ( S, A, B, E, Q ), в котором: начальное состояние s1 = s, конечное состояние sn Q, i &#x007B; 1, …, n &#x007D; (ai = ε) (bi = ε).

Определение 5.

Механизмом построения тестового сценария называется функция, значением которой является тестовый сценарий.

Механизмы построения тестового сценария применяются для создания тестовых сценариев на основе каких-либо данных. Примером такого механизма может быть последовательная композиция набора тестовых сценариев.

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

Тестовый сценарий в унифицированной архитектуре теста

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

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

Первый вид взаимодействия соответствует подаче стимула x

X и получению реакции y Y и постсостояния целевой системы v' V. Для осуществления такого взаимодействия тестовый сценарий обращается к оракулу, передавая ему стимул x X. Далее работа происходит по описанной ранее схеме. Оракул запоминает все необходимые части текущего модельного состояния v и передает стимул x медиатору. Медиатор оказывает тестовое воздействие, моделируемое посредством стимула x, получает реакцию целевой системы, преобразует ее в модельное представление y и синхронизирует текущее модельное состояние с внутренним состоянием реализации. Оракул, зная сохраненное состояние v, стимул x, реакцию y и текущее состояние v', выносит вердикт о корректности данного взаимодействия.

В качестве результата взаимодействия тестовый сценарий получает реакцию y

Y и постсостояния целевой системы v' V. Последнее передается неявным образом через модельное состояние. Тестовый сценарий, получив эти данные, обновляет свое состояние и принимает решение о следующем взаимодействии.

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

Второй вид взаимодействия соответствует подаче стимула v

V и "пустой" реакции целевой системы ε. В этом случае, тестовый сценарий обращается непосредственно к медиатору с указанием перевести целевую систему в состояние, соответствующее модельному состоянию v V.
Медиатор выполняет данное указание и соответствующим образом обновляет модельное состояние.

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

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

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



Рисунок 6. Тестовый сценарий в универсальной архитектуре теста

Унифицированная архитектура теста, дополненная тестовым сценарием, представлена на рисунке 6. Здесь стрелками обозначены направления передачи данных между компонентами тестовой системы.

Работа автоматного тестового сценария в случае тестирования со скрытым состоянием представлена на .

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

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



Медиатор выполняет данное указание и соответствующим образом обновляет модельное состояние.

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

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

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



Рисунок 6. Тестовый сценарий в универсальной архитектуре теста

Унифицированная архитектура теста, дополненная тестовым сценарием, представлена на рисунке 6. Здесь стрелками обозначены направления передачи данных между компонентами тестовой системы.

Работа автоматного тестового сценария в случае тестирования со скрытым состоянием представлена на .

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

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

Требования к полноте набора асинхронных реакций

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

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

Такого рода несоответствие между формальной оценкой корректности поведения и ожиданиями пользователя происходит по двум причинам:

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

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

Для выявления такого рода некорректностей можно предложить следующий подход. К множеству асинхронных реакций асинхронного интерфейса ( X, Y, Z ) добавляется вспомогательная асинхронная реакция done, семантика которой заключается в отражении того факта, что время, отведенное на получение асинхронных реакций, вышло. Соответственно, в асинхронную спецификацию добавляется спецификация псевдо интерфейсной операции Specdone, описывающая корректные переходы модели требований, помеченные реакцией done. Эти переходы предлагается интерпретировать следующим образом. Если из данного состояния модели требований v

V существует переход, помеченный асинхронной реакцией z Z, то

Второй подход основывается на использовании модели временных меток. Для этого к каждому асинхронному взаимодействию приписывается временной интервал, то есть в асинхронном интерфейсе целевой системы множества Y и Z заменяются на Y x TI(TM) и Z x TI(TM) соответственно. В этом случае, в спецификациях интерфейсных операций временные метки учитываются при описании требований ко времени получения реакций, посредством сохранения в модельном состоянии информации о времени осуществления соответствующих асинхронных воздействий. Во втором подходе также может потребоваться использование множества псевдо асинхронных реакций &#x007B; done &#x007D; x TI(TM) для отражения момента завершения сбора асинхронных реакций.

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

Рассмотренные методы организации проверки дополнительных требований к полноте набора асинхронных реакций и времени их появления построены на использовании ранее определенных моделей поведения и требований. Изменения касались только технологии использования этих моделей. Поэтому для реализации дополнительных проверок никаких изменений в моделях поведения и требований и алгоритмах работы с ними не требуется.

Унифицированная архитектура асинхронного теста

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

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

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

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

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

Унифицированная архитектура теста

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

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

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

Тестовая система содержит четыре компонента.

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

Все воздействия на целевую систему генерируемые тестовым сценарием осуществляется через оракул. Оракул

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

Медиатор получает от оракула указание осуществить тестовое воздействие, заданное стимулом x

X.
Для решения этой задачи медиатор

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

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

Управляемые метрики покрытия и оптимизация тестового набора

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

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

Управляющие автоматы

Первым шагом в формализации понятия тестового сценария является определение управляющих автоматов.

Определение 3.

Управляющим автоматом будем называть пятерку ( V, X, Y, E, Q ), где

S - множество состояний, X - множество стимулов, Y - множество реакций, E

V x X x Y x V - множество переходов, Q V - множество заключительных состояний.

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

Стимул s

X называется допустимым в состоянии u V абстрактного автомата A = ( V, X, Y, E ) (или управляющего автомата ( V, X, Y, E, Q ) ), если существует переход ( v, x, y, v' ) E, такой что v = u и x = s.

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

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

Управляющий автомат начинает свою работу в некотором начальном состоянии. Он выбирает один из допустимых в данном состоянии стимулов и подает его управляемой системе. Затем управляющий автомат получает ответную реакцию и переходит в состояние, которое приписано переходу с данными пресостоянием, стимулом и реакцией. Если таких состояний несколько, то новое состояние выбирается недетерминированным образом. Если новое состояние является заключительным, то работа управляющего автомата завершается. В противном случае, все вышеописанные действия повторяются в новом состоянии.

Последовательность переходов ( e1, e2, …, en ) абстрактного автомата A = ( V, X, Y, E ) (или управляющего автомата ( V, X, Y, E, Q ) ) называется путем, если для каждого i = 1, …, n-1 постсостояние перехода ei совпадает с пресостоянием перехода ei+1.
При этом мы будем говорить, что путь ведет из пресостояния перехода e1 в постсостояние перехода en.

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

Функционированием управляющего автомата ( V, X, Y, E, Q ) с начальным состоянием v0

V называется конечный или бесконечный путь &#x007B; ei = ( vi, xi, yi, v'i ) &#x007D;, удовлетворяющий следующим условиям:

если начальное состояние является заключительным (v0 Q), то путь является пустой последовательностью, если начальное состояние не является заключительным (v0 Q), то пресостояние первого перехода v1 совпадает с начальным состоянием v0, (v1 = v0), если путь является конечным и его длина больше нуля, то постсостояние последнего перехода является заключительным (vn Q), если заключительное состояние присутствует в пути, то путь является конечным и это состояние есть постсостояние последнего перехода.

Управляющие автоматы будут использоваться далее для определения понятия тестового сценария.

Взаимодействующие автоматы

Определение 13.

Взаимодействующим автоматом будем называть шестерку ( S, s0, X, Y, E, Q ), где

S - множество состояний, s0

S - начальное состояние, X - множество стимулов, Y - множество реакций, E S x ( X Y &#x007B;τ&#x007D; ) x S - множество переходов, которые мы будем называть

посылающими, если второй элемент перехода является стимулом, принимающими, если второй элемент перехода является реакцией, внутренним, если второй элемент перехода является τ;

Q

S - множество заключительных состояний.

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

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

Заметим, что множества стимулов и реакций могут пересекаться (X

Y ≠ Ø), и поэтому в определении множества переходов используется операция дизъюнктивного объединения. Для обозначения того факта, что сообщение является стимулом мы будем использовать символ !, помещаемый следом за элементом множества X (например, x!), а для обозначения принадлежности сообщения к множеству реакций будет использоваться символ ?: (например, y?).

Конечная последовательность переходов ( e1, e2, …, en ) взаимодействующего автомата A = ( S, s0, X, Y, E, Q ) называется путем, если для каждого i = 1, …, n-1 постсостояние перехода ei совпадает с пресостоянием перехода ei+1. При этом мы будем говорить, что путь ведет из пресостояния перехода e1 в постсостояние перехода en.

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

Путь ( e1, e2, …, en ) взаимодействующего автомата A = ( S, s0, X, Y, E, Q ) называется функционированием, если пресостоянием перехода e1 является начальное состояние s0, а постсостояние перехода en принадлежит множеству конечных состояний Q.

Предположим, что взаимодействующий автомат A = ( S, s0, X, Y, E, Q ) входит в состав распределенного взаимодействующего автоматов DA. Переходы автомата A ( s1, m, s2 ) E будем называть внутренними для DA, если сообщение m сокрыто в одной из систем взаимодействующих автоматов, входящей в состав DA. В противном случае, переходы будем называть внешними для DA.

Функционированием распределенного взаимодействующего автомата DA называется тройка ( E, , μ ), где

E - набор функционирований &#x007B; ( ei,1, ei,2, …, ei,n(i) ) &#x007D; всех взаимодействующих автоматов, входящих в DA; - частичный порядок на множестве всех переходов &#x007B; ei,j &#x007D;i, j=1,…,n(i) набора E; μ : &#x007B; ei,j &#x007D; &#x007B; ei,j &#x007D; - отображение на этом же множестве переходов;

при условии, что E, и μ удовлетворяют следующим ограничениям:

областью определения μ является множество всех принимающих переходов ei,j = ( s1, m?, s2 ) автомата A, сообщение m которых сокрыто в некоторой системе взаимодействующих автоматов SA, входящей в состав DA; для каждого такого перехода ei,j = ( s1, m?, s2 ) значением μ(ei,j) является посылающий переход ei',j' = ( s'1, m!, s'2 ) автомата A', входящего в состав той же системы взаимодействующих автоматов SA, но не совпадающего с A (A ≠ A'); частичный порядок сохраняет порядок переходов, относящихся к функционированию одного взаимодействующего автомата, то есть

ei,j, ei',j' &#x007B; ei,j &#x007D; (i = i') (j < j') ei,j ei',j'; переходы, связанные отношением μ, являются неразличимыми относительно частичного порядка , то есть

ei,j, ei',j' &#x007B; ei,j &#x007D; ei',j' = μ(ei,j)

e &#x007B; ei,j &#x007D; ( (e ei,j) (e ei',j') ) ( (ei,j e) (e i',j' e) ).

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

В настоящей работе рассмотрен метод

В настоящей работе рассмотрен метод тестирования систем с асинхронным интерфейсом, являющийся составной частью технологии UniTesK. В результате исследования подхода классических программных контрактов, лежащего в основе технологии UniTesK для тестирования синхронных систем, были выявлены основные проблемы, препятствующие его применению для тестирования систем с асинхронным интерфейсом. Эти проблемы заключаются в том, что базовые предположения относительно поведения целевой системы, лежащие в основе подхода, оказываются неприменимыми к системам с асинхронным интерфейсом.
Для систем с асинхронным интерфейсом оказывается не верно, что:
любое взаимодействие между тестируемой системой и ее окружением может инициироваться только окружением; все взаимодействия происходят строго последовательно, то есть следующее взаимодействие начинается только после завершения предыдущего.
По результатам исследования особенностей систем с асинхронным интерфейсом были разработаны новые математические модели, позволяющие корректным образом сформулировать основные задачи тестирования для систем с асинхронным интерфейсом, и были исследованы алгоритмы, решающие эти задачи. Ниже мы рассмотрим каждую задачу в отдельности.
Задача оценки корректности поведения целевой системы решается следующим образом:
требования к функциональности тестируемой системы описываются в виде формальных спецификаций, которые неявным образом задают автомат с отложенными реакциями; поведение целевой системы, наблюдаемое в процессе тестирования, представляется в виде частично-упорядоченного множества взаимодействий между целевой системой и ее окружением; зафиксированное множество взаимодействий проверяется на соответствие автомату с отложенными реакциями, заданному формальными спецификациями требований.
Если множество соответствует автомату, то считается, что поведение целевой системы в процессе тестирования удовлетворяло предъявляемым к нему требованиям. В противном случае считается, что тестирование обнаружило несоответствие между поведением целевой системы и формальными спецификациями требований.

---

---