Обход расширенного конечного автомата (EFSM, Extended Finite State Machine)¶

Веронский метод (Franco Fummi et al.)¶

Метод обхода EFSM состоит из трёх фаз:

1. обучение (learning);
2. случайный обход (random walk);
3. поиск с возвратами (backjumping).

Обучение¶

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

1. TODO: в одном графе представляются как зависимости по данным, так и зависимости по управлению?
2. TODO: зависимости по разным переменным представляются разными дугами?

Переход t ₂ зависит по данным от перехода t ₁, если t ₁ устанавливает значение некоторой переменной x (действие перехода содержит присваивание в x), а t ₂ использует x при вычислении значения другой переменной (внутренней или выходной).

Переход t ₂ зависит по управлению от перехода t ₁, если t ₁ устанавливает значение некоторой переменной x, которая входит в условие срабатывания t ₂.

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

Случайный обход¶

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

1. сброс состояния EFSM;
2. генерация входных векторов в цикле, пока не будет достигнута максимальная длина текущей последовательности.

Входной вектор генерируется следующим образом:

1. случайным образом выбирается один из переходов, исходящих из текущего состояния;
2. делается попытка разрешить его условие срабатывания;
3. если условие срабатывания разрешено:
   1. невовлечённым в него входным переменным присваиваются случайные значения;
   2. применяется действие перехода и обновляется состояние EFSM;
   3. выполненному переходу ставится в соответствие номер текущей последовательности и номер текущего её элемента.
      1. TODO: Переходу или состоянию?
4. если условие срабатывания не разрешено:
   1. TODO: Что делается в этом случае?

Поиск с возвратами¶

Составляется список непокрытых переходов, причём переходы, исходящие из посещённых на предыдущем этапе состояний, помещаются в начало списка. Затем циклически выполняются следующие действия:

1. выбирается переход из начала списка;
2. если его условие срабатывания зависит только от входных переменных:
   1. извлекается сохранённая на предыдущем шаге информация о достижимости начального состояния этого перехода;
   2. на основе этой информации к EFSM применяется соответствующая входная последовательность, и EFSM оказывается в начальном состоянии обрабатываемого перехода;
   3. разрешается условие срабатывания этого перехода;
      1. TODO: А если условие неразрешимо?
   4. переход удаляется из списка;
3. если его условие срабатывания зависит не только от входных переменных:
   1. извлекается сохранённая на предыдущем шаге информация о достижимости начального состояния этого перехода;
   2. на основе этой информации к EFSM применяется соответствующая входная последовательность, и EFSM оказывается в начальном состоянии обрабатываемого перехода; ## делается попытка разрешить условие срабатывания этого перехода:
      1. если она успешна, переход удаляется из списка;
      2. если нет — обработка продолжается;
4. на основании информации о зависимостях по данным извлекаются переходы, которые определяют значение переменных, входящих в условие срабатывания обрабатываемого перехода;
5. для каждого из них (пусть это будет t) выполняются следующие действия:
   1. получить информацию о достижимости начального состояния t, выполнить соответствующую тестовую цепочку;
      1. TODO: что делать, если начальное состояние t недостижимо?
   2. если переход t не обновляет значение счётчика, при помощи алгоритма Дейкстры найти путь от t к целевому переходу;
   3. если в t обновляется значение счётчика, алгоритм Дейкстры применяется два раза: сначала, чтобы найти путь от конечного состояния t до целевого перехода, а затем - чтобы найти путь из начального состояния t в самого себя через t;
   4. при помощи решателя ограничений определяется, сколько раз необходимо пройти по второму пути (то есть по циклу), чтобы начать двигаться по первому;
      1. TODO: как это делается?
   5. построить ограничение в виде композиции действия перехода t и условие срабатывания t и целевого перехода;
   6. если это ограничение неразрешимо:
      1. перейти к следующему t;
   7. если это ограничение разрешимо:
      1. подать полученные значения входных переменных в EFSM;
      2. последовательно пройти по каждому переходу из найденного алгоритмом Дейкстры пути;
      3. если условие срабатывания какого-либо из переходов неразрешимо:
         1. перейти к следующему t.

Литература¶

TODO: Дать ссылку на статью.