Пассивные последовательные системы
Примеры: большинство подсистем стандартной библиотеки libC.
Целевая система считается относящейся к данному классу, если она удовлетворяет следующим требованиям:
- в ответ на каждый подаваемый стимул она выдает пустую или немедленную реакцию;
- вне вызовов из тестовой системы целевая система не выполняет никаких действий и не меняет свое состояние;
- поставленная задача тестирования не включает проверку работы целевой системы в многопоточном окружении, или такая работа невозможна.
Исходно технология UniTesK разрабатывалась для тестирования именно данного класса систем. Рассмотрим вкратце способ тестирования, применяемый в данном случае.
При создании тестового сценария используется абстракция обобщенных состояний, где каждое обобщенное состояние соответствует некоторому классу эквивалентности реализационных состояний целевой системы. Обычно в модели обобщенных состояний используется значительно более высокий уровень абстракции, чем в модели, используемой для проверки корректности работы целевой системы. В любой момент времени целевая система находится в некотором однозначно определенном обобщенном состоянии и может изменить его только в результате применения тестового стимула. После применения некоторого стимула в некотором обобщенном состоянии целевой системы анализируется полученная реакция и вычисляется новое обобщенное состояние.
Задача тестового сценария состоит в обходе ребер ориентированного графа, вершины которого соответствуют обобщенным состояниям целевой системы, а ребра - применяемым к ней обобщенным стимулам, где каждый обобщенный стимул соответствует некоторому классу эквивалентности возможных стимулов, применяемых к целевой системе. Граф строится интерактивно, по мере выполнения теста, на основе правил вычисления текущего обобщенного состояния целевой системы и правил перебора стимулов, применяемых в зависимости от обобщенного состояния.
Модель обобщенного состояния и обобщенных стимулов строится так, чтобы при повторном применении обобщенного стимула в некотором обобщенном состоянии целевая система всегда переводилась в то же самое обобщенное состояние, в которое она ранее переходила при применениях этого стимула в том же состоянии. Также накладывается дополнительное требование сильной связности графа обобщенных состояний. Практика тестирования реальных систем показывает, что для систем, удовлетворяющих минимальным требованиям к детерминизму поведения, построение модели, удовлетворяющей изложенным требованиям, возможно.
Способы тестирования, применяемые в технологии UniTesK для данной конфигурации активных потоков, более подробно описаны в [, ]. Случай недетерминированного поведения целевой системы частично рассматривается ниже, но в целом выходит за рамки данной работы []
