Project

General

Profile

Actions

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

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

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

Обучение

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

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

Переход t 2 зависит по управлению от перехода t 1 через переменную x, если t 1 устанавливает (defines) значение x, а t 2 использует (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. извлекается сохранённая на предыдущем шаге информация о достижимости начального состояния этого перехода;
  3. на основе этой информации к EFSM применяется соответствующая входная последовательность, и EFSM оказывается в начальном состоянии обрабатываемого перехода;
  4. делается попытка разрешить условие срабатывания этого перехода:
  5. если она успешна:
    1. полученный входной вектор добавляется в новую тестовую последовательность;
    2. сохраняется информация о достижимости целевого перехода;
    3. его обработка заканчивается;
  6. на основании информации о зависимостях по данным извлекаются переходы, которые определяют значение переменных, входящих в условие срабатывания обрабатываемого перехода;
  7. для каждого из них (пусть это будет t) выполняются следующие действия:
    1. получить информацию о достижимости начального состояния t, выполнить соответствующую тестовую цепочку (если начальное состояние t не было достигнуто ранее, то делается попытка достигнуть его при помощи механизма обратных переходов);
    2. если начальное состояние t недостижимо, перейти к следующему за t элементу списка;
    3. если переход t не обновляет значение счётчика, при помощи алгоритма Дейкстры найти путь от t к целевому переходу;
    4. если в t обновляется значение счётчика, алгоритм Дейкстры применяется два раза: сначала, чтобы найти путь от конечного состояния t до целевого перехода, а затем - чтобы найти путь из начального состояния t в самого себя через t; при помощи решателя ограничений определяется, сколько раз необходимо пройти по второму пути (то есть по циклу), чтобы начать двигаться по первому;
    5. строится ограничение в виде конъюнкции действия перехода t и условие срабатывания t и целевого перехода;
    6. если это ограничение неразрешимо:
      1. перейти к следующему t;
    7. если это ограничение разрешимо:
      1. подать полученные значения входных переменных в EFSM;
      2. последовательно пройти по каждому переходу из найденного алгоритмом Дейкстры пути;
      3. если условие срабатывания какого-либо из переходов неразрешимо:
        1. перейти к следующему t.

Литература

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

Updated by Alexander Kamkin about 5 years ago · 13 revisions