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

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

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

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

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

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

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

Нарушение предусловий асинхронных воздействий

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

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

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

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

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

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

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

Если предусловие интерфейсной операции задано предикатом pre_I на множестве V_I x X_I, то статической составляющей предусловия мы будем называть предикат static(pre_I) на множестве X_I, определяемый следующим образом:

static(pre_I)(x) = T v V_I pre_I(v,x) = T

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

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

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

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

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

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

Оценка качества тестирования

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

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

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

Метрики покрытия асинхронной модели требований

Метрикой покрытия асинхронной модели требований A = ( V, X, Y, Z, E ) называется конечное множество подмножеств переходов модели требований M 2^E . Элементами покрытия называются элементы метрики M, являющиеся подмножествами E.

Частично-упорядоченное множество ( P', ' ) называется префиксным подмножеством частично-упорядоченного множества ( P, ), если:

• множество P' является подмножеством P ( P' P );
• частичный порядок ' является подмножеством частичного порядка ' (' );
• все пары элементов из P', являющиеся упорядоченными в ( P, ), также являются упорядоченными в ( P', ' ):
  (p₁,p₂) p₁ P' p₂ P' (p₁,p₂) ' ;
• все элементы P меньшие элемента P' также принадлежат P':
  (p₁,p₂) ; p₂ P' p₁ P'.

Предположим, что асинхронный тест ( P, ) является неуспешным относительно асинхронной модели требований A = ( V, X, Y, Z, E ) с начальным состоянием v₀ V. Будем говорить, что частично-упорядоченное множество ( P', ' ) является граничным успешным подтестом асинхронного теста ( P, ), если:

• ( P', ' ) является префиксным подмножеством ( P, );
• ( P', ' ) является успешным относительно асинхронной модели требований A = ( V, X, Y, Z, E ) с начальным состоянием v₀ V;
• существует такое частично-упорядоченное множество ( P'', '' ), что
  • ( P'', '' ) является префиксным подмножеством ( P, );
  • ( P'', '' ) является неуспешным относительно асинхронной модели требований A = ( V, X, Y, Z, E ) с начальным состоянием v₀ V;
  • P'' включает в себя P', но P'' больше P' ровно на один элемент ( P' ⊂ P'' | P'' \ P' | = 1 ).

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

Если асинхронный тест ( P, ) является успешным относительно асинхронной модели требований A = ( V, X, Y, Z, E ) с начальным состоянием v₀ V, то путь в автомате A, удовлетворяющий требованиям определения 9 будем называть успешным.

Если асинхронный тест ( P, ) является успешным относительно асинхронной модели требований A = ( V, X, Y, Z, E ) с начальным состоянием v₀ V, то будем говорить, что тест ( P, ) покрыл элемент покрытия C_j M, если любой успешный путь ( e₁, e₂, …, e_n, … ) теста ( P, ) в автомате A содержит хотя бы один переход e_i, входящий во множество C_j.

Если асинхронный тест ( P, ) является неуспешным относительно асинхронной модели требований A = ( V, X, Y, Z, E ) с начальным состоянием v₀ V, то будем говорить, что тест ( P, ) покрыл элемент покрытия C_j M, если любой успешный путь ( e₁, e₂, …, e_n, … ) любого граничного успешного подтеста теста ( P, ) в автомате A содержит хотя бы один переход e_i, входящий во множество C_j.

Покрытием метрики M асинхронным тестом ( P, ) будем называть набор элементов метрики M, покрытых данным тестом.

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

Асинхронная метрика покрытия M называется управляемой, если все переходы из ее элементов, помечены стимулом и непосредственной реакцией, и для любых двух переходов I₁ = ( v₁, x₁, y₁, v'₁ ) и I₂ = ( v₂, x₂, y₂, v'₂ ) выполнено следующее утверждение:

(v₁ = v₂) (x₁ = x₂) C_i M (I₁ C_i) (I₂ C_i)

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

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

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

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

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

MA[μ] = { C_r 2^E | r R }, где C_r = { ( v, x, y, v' ) V x X x Y x V | μ( v, x, y, v' ) = r}.

Аналогично определяются метрики покрытия интерфейсных операций-реакций. Метрика покрытия интерфейсной операции μ : V_Rj x Unit x Y_Rj x V_Rj R используется для описания асинхронной метрики интерфейсной операции-реакции R_j. Этой метрике μ соответствует асинхронная метрика покрытия MA[μ] асинхронной модели требований MRA[Spec]:

MA[μ] = { C_r 2^E | r R }, где C_r = { ( v, z, v' ) V x Z x V | μ( v, ε, z, v' ) = r}.

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

Второй способ описания метрик покрытия при помощи расширенных метрик покрытия интерфейсных операций также может быть использован при тестировании асинхронных систем. Асинхронная метрика покрытия, заданная посредством расширенной метрики покрытия интерфейсной операции S_i μ' = { c_p | p = 1, …, n; c_p : V_Si x X_Si x Y_Si x V_Si Bool }, обозначается MA[μ']:

M[μ'] = { C_p 2^E | p = 1, …, n }, где C_p = { ( v, x, y, v' ) V x X x Y x V | c_p( v, x, y, v' ) }.

Также как и асинхронная метрика покрытия, заданная посредством расширенной метрики покрытия интерфейсной операции R_j μ' = { c_p | p = 1, …, n; c_p : V_Rj x Unit x Y_Rj x V_Rj Bool }:

M[μ'] = { C_p 2^E | p = 1, …, n }, где C_p = { ( v, z, v' ) V x Z x V | c_p( v, ε, z, v' ) }.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

4. Инструментальная поддержка тестирования систем с асинхронными интерфейсами

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

• доступ для чтения;
• доступ для записи;
• доступ для обновления.

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

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

Постусловие представляется собой составной оператор, помеченный ключевым словом SEC post. Код внутри составного оператора эквивалентен коду функции языка C, имеющей возвращаемое значение типа bool, а также набор параметров, состоящий из

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

На третьем шаге разработки тестового набора решаются три задачи:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Реализация протокола IPv6

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

Асинхронность взаимодействий реализации 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. Такая последовательность пакетов может быть использована для организации атаки типа "Отказ в обслуживании".

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

Функциональность протокола Mobile IPv6

Работа по тестированию MSR IPv6 получила продолжение в проекте по тестированию функций Mobile IPv6 на примере реализации Microsoft MIPv6 для Windows CE 4.1 и Windows XP. В этом проекте было проведено тестирование соответствия реализации базовых функций IPv6 в Windows CE на основе спецификаций и тестов, разработанных для MSR IPv6. Кроме того, проводилось тестирование на соответствие реализации ряда функций протокола Mobile IPv6 спецификациям протокола, а также соответствие реализации служебного протокола MLD (Multicast Listener Discovery) спецификации протокола.

Требования к реализации Mobile IPv6 извлекались из 13-го проекта стандарта Mobile IPv6, так как именно эту спецификацию поддерживала тестируемая реализация. Требования к реализации MLD извлекались из спецификаций первой версии протокола MLD, RFC 2710. В качестве дополнительных источников требований использовались RFC 2462 и RFC 2473. Эти требования были описаны в виде асинхронной модели требований, которая в дальнейшем использовалась для оценки корректности поведения тестируемой системы.

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

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

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

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

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

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

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

Компоненты распределенной операционной системы для сенсорных сетей

В дополнение к опыту тестирования телекоммуникационных систем предложенный подход применялся для тестирования асинхронных аспектов поведения многопроцессных и многопотоковых систем. Первым таким опытом был пилотный проект по тестированию отдельных компонентов TinyOS - распределенной операционной системы для сенсорных сетей, проведенной ИСП РАН совместно с российской компанией Luxoft.

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

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

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

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

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

Ядро операционной системы реального времени

Наиболее значимой работой по тестированию асинхронных аспектов поведения многопотоковых и многопроцессных систем является проект по тестированию ядра POSIX-совместимой операционной системы реального времени ОС2000. Эта операционная система предоставляет пользователю прикладной программный интерфейс, состоящий из 482 функций. В рамках проекта все функции были проанализированы и сгруппированы по подсистемам согласно реализуемой ими функциональности. Список подсистем приведен в таблице 2. Во втором столбце таблицы указано число интерфейсных функций, принадлежащих соответствующей подсистеме.

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

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

Подсистема управления потоками содержит такие асинхронные реакции как:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

6. Заключение

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

Для систем с асинхронным интерфейсом оказывается не верно, что:

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

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

Задача оценки корректности поведения целевой системы решается следующим образом:

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

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

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

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

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

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

Предложенный метод и его инструментальная поддержка были апробированы в шести проектах по тестированию различного программного обеспечения. В качестве тестируемых систем выступали реализации протоколов IPv6, Mobile IPv6, MPEG-2 IPMP, отдельные компоненты распределенной операционной системы для сенсорных сетей TinyOS, ядро операционной системы реального времени ОС2000 и функции стандартного бинарного интерфейса операционной системы Linux. Вышеозначенные проекты показали востребованность методов тестирования систем с асинхронным интерфейсом, а также работоспособность предложенных решений и их программной реализации, обеспечивших проведение систематизированного тестирования таких сложных асинхронных систем, как операционные системы и реализации телекоммуникационных протоколов.

Литература

1.обратно	Euler E.E., Jolly S.D., Curtis H.H. The Failures of the Mars Climate Orbiter and Mars Polar Lander: A Perspective from the People Involved // Proceedings of Guidance and Control 2001. American Astronautical Society, AAS 01-074, 2001.
2.обратно	Report on the Loss of the Mars Climate Orbiter Mission. JPL D-18441, 1999.
3.обратно	Porrello A.M. Death and Denial: The Failure of the Therac-25, A Medical Linear Accelerator.
4.обратно	Leveson N.G., Clark S.T. An Investigation of the Therac-25 Accidents // Computer. July, 1993. P. 18-41.
5.обратно	Patriot missile defense: Software problems led to system failure at Dhahran, Saudi Arabia. Report GAO/IMTEC-92-26, Information Management and Technology Division, US General Accounting Office. Washington DC, Feb. 11992.
6.обратно	Berry D. M. Formal methods: the very idea, some thoughts about why they work when they work. // Science of Computer Programming #42(1). P. 11-27.
7.обратно	Floyd R. W. Assigning meanings to programs // Proceedings Symp. Appl. Math., 19. in: J.T.Schwartz (ed.), Mathematical Aspects of Computer Science. P. 19-32. American Mathematical Society, Providence, R.I., 1967.
8.обратно	Francez N. Verification of programs. Addison-Wesley Publishers Ltd., 1992.
9.обратно	Manna Z. Mathematical theory of computation. McGraw-Hill, 1974.
10.обратно	Manna Z., Pnueli A. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, 1991.
11.обратно	Blackburn M., Busser R., Nauman A., Knockerbocker R., Kasuda R. Mars Polar Lander Fault Identification Using Model-Based Testing // 26th Annual NASA Goddard Software Engineering Workshop. 27-29 November, 2001.
12.обратно	Dalal S. R., Jain A., Karunanithi N., Leaton J. M., Lott C. M. Model-Based Testing of a Highly Programmable System // Proceedings of ISSRE-98. 5-7 November 1998.
13.обратно	Dalal S. R., Jain A., Karunanithi N., Leaton J. M., Lott C. M., Patton G. C., Horowitz B. M. Model-Based Testing in Practice // Proceedings of the ICSE'99. May 1999.
14.обратно	Farchi E., Hartman A., Pinter S. S. Using a Model-Based Test Generator to Test for Standard Conformance // IBM Systems Journal, 2002. V. 41, No. 1, P. 89-110.
15.обратно	Gronau A., Hartman A., Kirshin A., Nagin K., Olvovsky S. A Methodology and Architecture for Automated Software Testing // IBM Research Laboratory in Haifa Technical Report, 2000.
16.обратно	Offutt A. J., Liu S., Abdurazik A. Generating Test Data from State-Based Specifications // Journal of Software Testing, Verification & Reliability. V. 13, No. 1, March 2003.
17.обратно	Al-Ghafees M., Whittaker J. A. Markov Chain-based Test Data Adequacy Criteria: a Complete Family. // IS June 2002. P. 13-37.
18.обратно	Bourdonov I., Kossatchev A., Kuliamin V., Petrenko A. UniTesK Test Suite Architecture // Proceedings of FME, 2002. LNCS 2391. P. 77-88. Springer-Verlag.
19.обратно	Кулямин В.В., Петренко А.К., Косачев А.С., Бурдонов И.Б. Подход UniTesK к разработке тестов // Программирование, 29(6). 2003. С. 25-43.
20.обратно	Баранцев А.В., Бурдонов И.Б., Демаков А.В., Зеленов С.В., Косачев А.С., Кулямин В.В., Омельченко В.А., Пакулин Н.В., Петренко А.К., Хорошилов А.В. Подход UniTesK к разработке тестов: достижения и перспективы // Труды Института системного программирования РАН, №5, 2004. [HTML].
21.обратно	Meyer B. Applying 'Design by Contract' // IEEE Computer, vol. 25, October 1992. P. 40 51.
22.обратно	http://www.unitesk.com[HTML,PDF].
23.обратно	Burdonov I., Kossatchev A., Petrenko A., Cheng S., Wong H. Formal Specification and Verification of SOS Kernel // BNR, NORTEL Design Forum, June 1996.
24.обратно	Monin J. F., Hinchey M. G. Understanding Formal Methods. Springer-Verlag, 2003.
25.обратно	Бурдонов И.Б., Косачев А.С., Кулямин В.В. Использование конечных автоматов для тестирования программ. // Программирование, 2000, №2.
26.обратно	Бурдонов И.Б., Косачев А.С., Кулямин В.В. Неизбыточные алгоритмы обхода ориентированных графов. Детерминированный случай. // Программирование. 2003. №5. С. 11 30.
27.обратно	Бурдонов И.Б., Косачев А.С., Кулямин В.В. Неизбыточные алгоритмы обхода ориентированных графов. Недетерминированный случай. // Программирование. 2004. №1. С. 4 24.
28.обратно	Бурдонов И.Б., Косачев А.С., Кулямин В.В. Асинхронные автоматы: классификация и тестирование. // Труды ИСП РАН. 2003. №4. С. 7 84.
29.обратно	Хорошилов А.В. Спецификация и тестирование компонентов с асинхронным интерфейсом. Диссертация на соискание ученой степени кандидата физико-математических наук. Москва, ИСП РАН, 2006.
30.обратно	Липский В. Комбинаторика для программистов. Москва, Мир, 1988.
31.обратно	Message Sequence Charts. ITU recommendation Z.120.
32.обратно	Agamirzian I., Groshev S.G., Khoroshilov A.V., Kluchnikov G.N., Kossatchev A.S., Omelchenko V.A., Pakoulin N.V., Petrenko A.K., Shnitman V.Z. MSR IPv6 verification project, December 2001. [HTML].
33.обратно	Agamirzian I., Groshev S.G., Khoroshilov A.V., Kluchnikov G.N., Kossatchev A.S., Omelchenko V.A., Pakoulin N.V., Petrenko A.K., Shnitman V.Z. MSR IPv6 Verification within the CTesK-lite Framework, April 2002. [HTML].
34.обратно	http://www.linuxtesting.ru[HTML].
35.обратно	Linux Standard Base Core 3.1. ISO/IEC IS-23360. [HTML].

---

1(обратно к тексту)	В данной работе рассматриваются только не более чем счетные множества.
2(обратно к тексту)	Здесь под процессом тестирования понимается процесс выполнения уже разработанного теста. Если под процессом тестирования понимать процесс разработки теста, то данное утверждение будет не совсем верно.
3(обратно к тексту)	Данные правила приводятся только для целей иллюстрации, поэтому их определение дано на поверхностном уровне, не рассматриваются вопросы, касающиеся области их применимости, и т.д.
4(обратно к тексту)	Множества Xstack, Ystack и Vstack определяются с точностью до изоморфизма.
5(обратно к тексту)	В указанной работе этот алгоритм обозначается символом A2.
6(обратно к тексту)	Определение обозначений XI, YI и VI смотрите в разделе "Описание модели требований".
7(обратно к тексту)	Более детальное обсуждение проблемы нарушения предусловия интерфейсных операций-стимулов смотрите в разделе "Нарушение предусловий асинхронных воздействий".
8(обратно к тексту)	Здесь и далее идентификатор Unit будет обозначать множество, состоящее из единственного элемента e, а идентификатор Bool - множество, состоящее из двух элементов true и false.
9(обратно к тексту)	В рамках данного доказательства мы считаем, что ei = ( vi, xi, v'i ).