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

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

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

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

Обучение¶

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

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

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

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

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

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

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

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

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

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

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

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.

Литература¶

http://link.springer.com/article/10.1007%2Fs10836-011-5209-8