Тестирование X-машины

Методология (Stream) X-Machine Testing — это комплексный функциональному тестированию подход к программного и аппаратного обеспечения. который использует масштабируемость Stream X-Machine . модели вычислений Используя эту методологию, можно определить конечный набор тестов, который исчерпывающе определит, соответствует ли реализация тестируемой системы ее спецификации. Эта цель достигается с помощью подхода «разделяй и властвуй», при котором проект разлагается путем уточнения. в коллекцию Stream X-Machines , которые реализованы как отдельные модули, а затем протестированы снизу вверх. На каждом этапе интеграции метод тестирования гарантирует правильную интеграцию тестируемых компонентов.

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

Мотивация

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

• Полное положительное тестирование: подтверждает, что в системе присутствует все желаемое поведение;
• Полный отрицательный результат тестирования: подтверждает отсутствие непреднамеренного поведения в системе.

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

,

Майк Холкомб впервые предложил использовать Сэмюэля Эйленберга теоретическую модель X-машины в качестве основы для спецификации программного обеспечения в конце 1980-х годов. Это связано с тем, что модель четко отделяет поток управления системой от обработки , выполняемой системой. На данном уровне абстракции систему можно рассматривать как простой конечный автомат, состоящий из нескольких состояний и переходов. Более сложная обработка делегируется функциям обработки переходов, которые изменяют базовый фундаментальный тип X. данных Позже каждая функция обработки может быть представлена ​​отдельно и охарактеризована другой X-машиной , моделирующей поведение этой системной операции.

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

Спецификации, подлежащие постепенному тестированию

Гилберт Лэйкок первым предложил особый вид X-машины , Stream X-Machine , в качестве основы для метода тестирования. Преимуществом этого варианта был способ контроля тестирования. В Stream X-Machine фундаментальный тип данных имеет конкретную форму: X = Out * × Mem × In *, где In * — входной поток, Out * — выходной поток, а Mem — внутренняя память. Переходы Stream X-Machine помечены функциями обработки вида φ: Mem × In → Out × Mem , то есть они потребляют один вход из входного потока, возможно, изменяют память и производят один выход в выходном потоке. ( см. в соответствующей статье более подробную информацию ).

Преимущества тестирования заключаются в том, что разработанные таким образом программные системы можно наблюдать на каждом этапе. Для каждого ввода машина делает один шаг, создавая результат, так что пары ввода/вывода могут точно совпадать. Это контрастирует с другими подходами, в которых система работает до завершения (выполняя несколько шагов) до того, как будет сделано какое-либо наблюдение. Более того, многоуровневые Stream X-Machines предлагают удобную абстракцию. На каждом уровне тестер может забыть о деталях функций обработки и рассматривать (под)систему просто как простой конечный автомат . Существуют мощные методы тестирования систем, которые соответствуют спецификациям конечного состояния, такие как W-метод Чоу.

Метод спецификации

При использовании методологии (Stream) X-Machine первым этапом является определение различных типов данных, подлежащих обработке. Например, текстовый процессор будет использовать базовые типы «Символ» (ввод с клавиатуры), «Позиция» (положение курсора мыши) и «Команда» (команда мыши или меню). Могут быть и другие сконструированные типы, такие как Текст ::= Символ * (последовательность символов), Выбор ::= Позиция × Позиция (начало и конец выделения) и Документ ::= Текст × Выбор × Логическое значение ( текст, возможный выбор и флаг, сигнализирующий о том, что документ был изменен).

высокого

Спецификация верхнего уровня — это Stream X-Machine, описывающий основное взаимодействие пользователя с системой. Например, текстовый процессор будет находиться в нескольких состояниях, в которых нажатия клавиш и команды будут иметь разные эффекты. Предположим, что этот текстовый процессор существует в состояниях { Написание , Выбор , Сохранение , Редактирование }. Мы ожидаем, что текстовый процессор запустится в исходном состоянии «Письмо» , но перейдет в состояние «Выбор» мышь , если перетащить или клавишу Shift удерживать . Как только выбор будет установлен, он должен вернуться в состояние записи . Аналогично, если выбран пункт меню, он должен перейти в состояние «Редактирование» или «Сохранение» . В этих состояниях определенные нажатия клавиш могут иметь разное значение. Текстовый процессор в конечном итоге возвращается в состояние записи после завершения любой команды меню. Этот конечный автомат спроектирован и неформально помечен различными действиями, которые заставляют его изменять состояние.

Типы ввода, памяти и вывода для машины верхнего уровня теперь формализованы. Предположим, что тип памяти простого текстового процессора — это тип Document, определенный выше. При этом документ рассматривается как текстовая строка с двумя позициями, обозначающими возможный выбор, и флагом, указывающим на изменение с момента последней команды сохранения . Более сложный текстовый процессор может поддерживать отмену редактирования с последовательностью состояний документа: Документ ::= ( Текст × Выбор )*, которые сворачиваются в один документ каждый раз при сохранения выполнении команды .

Предположим, что тип ввода для машины: In ::= Команда × Символ × Позиция . При этом учитывается, что каждое взаимодействие может представлять собой простую вставку символов, команду меню или размещение курсора. Любое данное взаимодействие представляет собой тройку кортежей, но некоторые места могут быть пустыми. Например, ( Insert , 'a', ε) будет означать ввод символа 'a'; while ( Position , ε, 32) будет означать размещение курсора между символами 32 и 33; и ( Select , ε, 32) будет означать выбор текста между текущей позицией курсора и местом между символами 32 и 33.

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

Низкоуровневая

Если система сложная, то она, скорее всего, будет декомпозирована на несколько Stream X-Machines . Самый распространенный вид уточнения — взять каждую из основных функций обработки (которые были метками на машине высокого уровня) и рассматривать их как отдельные Stream X-Machines . В этом случае типы ввода, памяти и вывода для машин низкого уровня будут отличаться от тех, которые определены для машины высокого уровня. Либо это рассматривается как расширение наборов данных, используемых на высоком уровне, либо происходит перевод более абстрактных наборов данных на высоком уровне в более подробные наборы данных на более низком уровне. Например, команду Select на верхнем уровне можно разложить на три события: MouseDown , MouseMove , MouseUp на нижнем уровне.

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

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

Условия проектирования для испытаний

Методология (Stream) X-Machine требует от проектировщика соблюдения определенной конструкции для условий испытаний. Обычно их не так уж сложно удовлетворить. Для каждого Stream X-Machine в спецификации мы должны получить:

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

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

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

Метод тестирования

Метод (потокового) X-машинного тестирования предполагает, что и проект, и реализацию можно рассматривать как (набор) потоковых X-машин . Для каждой пары соответствующих машин ( Spec , Imp ) цель тестирования — определить, точно ли поведение Imp , машины реализации, точно соответствует поведению Spec , машины спецификации. Обратите внимание, что Imp не обязательно должен быть минимальной машиной — он может иметь больше состояний и переходов, чем Spec , и при этом вести себя идентично.

Чтобы протестировать любое поведение, необходимо иметь возможность перевести машину во все ее состояния, а затем попытаться выполнить все возможные переходы (те, которые должны быть успешными, и те, которые должны быть заблокированы), чтобы добиться полного положительного и отрицательного тестирования (см. выше). Для успешных переходов необходимо также проверить состояние назначения. Обратите внимание: если Spec и Imp имеют одинаковое количество состояний, приведенное выше описывает наименьший набор тестов, который достигает цели. Если в Imp больше состояний и переходов, чем в Spec , необходимы более длинные тестовые последовательности, чтобы гарантировать, что избыточные состояния в Imp также ведут себя должным образом.

Тестирование всех состояний

Основой стратегии генерации тестов является W-метод Цуна С. Чоу для тестирования автоматов с конечным состоянием. выбран потому, что он поддерживает тестирование избыточных реализаций. Метод Чоу предполагает простые конечные автоматы с наблюдаемыми входами и выходами, но без непосредственно наблюдаемых состояний. Чтобы отобразить формализм Чоу, функции φ _i на переходах потоковых X-машин рассматриваются просто как метки (входные данные, в терминах Чоу), а различающие выходные данные используются напрямую. отображение реальных входных данных и памяти ( mem , in (Позже выбирается ) для запуска каждой функции φ в соответствии с ее областью определения).

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

Чтобы достичь каждого состояния, ожидаемого в Spec , тестер создает покрытие состояний C — наименьший набор тестовых последовательностей, которые достигают каждого состояния. Это можно создать путем автоматического исследования Spec в ширину . набор тестов, который проверяет все состояния минимального беса : Тогда $C\otimes W$, где $\otimes$ обозначает объединенное произведение двух наборов. Например, если C = { ⟨ a ⟩ , ⟨ b ⟩ } и W = { ⟨ c ⟩ , ⟨ d ⟩ }, то $C\otimes W=\{\langle ac\rangle ,\langle ad\rangle ,\langle bc\rangle ,\langle bd\rangle \}$.

Тестирование всех переходов

Приведенный выше набор тестов определяет, имеет ли минимальный Imp те же состояния, что и Spec . Чтобы определить, имеет ли минимальный Imp такое же поведение перехода, как Spec , тестер создает покрытие перехода K . Это наименьший набор тестовых последовательностей, который достигает каждого состояния, а затем один раз пытается выполнить каждый возможный переход из этого состояния. Теперь входной алфавит состоит из (меток) каждой функции φ из Φ. Построим набор тестовых последовательностей длины 1, состоящий из отдельных функций, выбранных из Φ, и назовем его Φ ₁ . Переходное покрытие определяется как $K:=C\cup C\otimes \Phi _{1}$.

При этом будут предприняты все возможные переходы из каждого состояния. Для тех, кто преуспел, мы должны проверить состояния назначения. Итак, наименьший набор тестов T ₁ , который полностью подтверждает поведение минимального Imp, определяется следующим образом: $T_{1}::=C\otimes W\cup C\otimes \Phi _{1}\otimes W$. Эту формулу можно переписать так:

$T_{1}::=C\otimes \left(\Phi _{0}\cup \Phi _{1}\right)\otimes W$,

где Φ ₀ — множество, содержащее пустую последовательность { ⟨⟩ }.

Если у Imp больше состояний, чем у Spec , приведенного выше набора тестов может быть недостаточно, чтобы гарантировать согласованное поведение реплицированных состояний в Imp . Итак, выбираются наборы более длинных тестовых последовательностей, состоящих из всех пар функций Ф2 _, всех троек функций Ф3 _до некоторого предела _Фк , когда тестер удостоверяется, что Imp не может содержать цепочки дублированных состояний длиной более k -1. . Окончательная формула теста имеет вид:

$T_{\mathrm {k} }::=C\otimes \left(\Phi _{0}\cup \Phi _{1}\ldots \cup \Phi _{\mathrm {k} }\right)\otimes W$.

Этот набор тестов полностью подтверждает поведение неминимального Imp , в котором ожидается, что цепочки дублированных состояний будут не длиннее k -1. Для большинства практических целей тестирование до k =2 или k =3 является весьма исчерпывающим и выявляет все ошибки, связанные с состоянием, в действительно плохих реализациях.