Спецификация непроцедурных стимулов
Алгоритм обхода графа состояний автомата тестового сценария, реализованный в CTesK-lite, требует, чтобы воздействия на целевую систему оказывались только в стационарных состояниях. Протокол IPv6 не удовлетворяет указанному ограничению, так как некоторые внешние воздействия (входящие пакеты) могут оказываться в нестационарных состояниях. Например, в протоколе ICMPv6 Echo узел испускает пакет ICMPv6 Echo Request и переходит в нестационарное состояние, в котором ожидает входящего пакета ICMPv6 Echo Reply. Таким образом, внешнее воздействие – пакет ICMPv6 Echo Reply – необходимо оказать в нестационарном состоянии.
Для того, чтобы обойти ограничение на стационарность начального состояния, непроцедурные стимулы были специфицированы как отложенные реакции на некоторые процедурные стимулы. Мы ввели стимул “Отправить пакет IPv6 в целевую систему”. Спецификация для данного стимула тривиальна. Медиатор для данного стимула отправляет пакет IPv6 с удаленного узла. Собственно входящий пакет рассматривается как отложенная реакция на данный стимул.
