EFSM Traversal » History » Revision 6
Revision 5 (Alexander Kamkin, 02/28/2014 06:17 AM) → Revision 6/13 (Alexander Kamkin, 02/28/2014 06:18 AM)
h1. Обход расширенного конечного автомата (EFSM, Extended Finite State Machine)
h2. Веронский метод (Franco Fummi et al.)
Метод обхода EFSM состоит из трёх фаз:
# обучение (learning);
# случайный обход (random walk);
# поиск с возвратами (backjumping).
h3. Обучение
В ходе первой фазы анализируются _зависимости_ переходов 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_ называется _счетчиком_, если существует цикл (*TODO: в графе состояний EFSM или в графе зависимостей?*), в который входит переход с условием срабатывания, зависящим от _x_, а также переход, в действии которого меняется значение _x_, причем значение _x_ прямо или косвенно зависит от предыдущего значения _x_.
h3. Случайный обход
На вход случайного обходчика подаётся два параметра: количество тестовых последовательностей и длина каждой последовательности. В цикле, пока количество тестовых последовательностей не достигнет максимального числа или пока не будут покрыты все переходы выполняются следующие действия:
# сброс состояния EFSM;
# генерация входных векторов в цикле, пока не будет достигнута максимальная длина текущей последовательности.
Входной вектор генерируется следующим образом:
# случайным образом выбирается один из переходов, исходящих из текущего состояния;
# делается попытка разрешить его условие срабатывания;
# если условие срабатывания разрешено:
## невовлечённым в него входным переменным присваиваются случайные значения;
## применяется действие перехода и обновляется состояние EFSM;
## выполненному переходу ставится в соответствие номер текущей последовательности и номер текущего её элемента.
### *TODO: Переходу или состоянию?*
# если условие срабатывания не разрешено:
## *TODO: Что делается в этом случае?*
h3. Поиск с возвратами
Составляется список непокрытых переходов, причём переходы, исходящие из посещённых на предыдущем этапе состояний, помещаются в начало списка. Затем циклически выполняются следующие действия:
# выбирается переход из начала списка;
# если его условие срабатывания зависит только от входных переменных:
## извлекается сохранённая на предыдущем шаге информация о достижимости начального состояния этого перехода;
## на основе этой информации к EFSM применяется соответствующая входная последовательность, и EFSM оказывается в начальном состоянии обрабатываемого перехода;
## разрешается условие срабатывания этого перехода;
### *TODO: А если условие неразрешимо?*
## переход удаляется из списка;
# если его условие срабатывания зависит не только от входных переменных:
## извлекается сохранённая на предыдущем шаге информация о достижимости начального состояния этого перехода;
## на основе этой информации к EFSM применяется соответствующая входная последовательность, и EFSM оказывается в начальном состоянии обрабатываемого перехода; ## делается попытка разрешить условие срабатывания этого перехода:
### если она успешна, переход удаляется из списка;
### если нет — обработка продолжается;
# на основании информации о зависимостях по данным извлекаются переходы, которые определяют значение переменных, входящих в условие срабатывания обрабатываемого перехода;
# для каждого из них (пусть это будет _t_) выполняются следующие действия:
## получить информацию о достижимости начального состояния _t_, выполнить соответствующую тестовую цепочку;
### *TODO: что делать, если начальное состояние _t_ недостижимо?*
## если переход _t_ не обновляет значение счётчика, при помощи алгоритма Дейкстры найти путь от _t_ к целевому переходу;
## если в _t_ обновляется значение счётчика, алгоритм Дейкстры применяется два раза: сначала, чтобы найти путь от конечного состояния _t_ до целевого перехода, а затем - чтобы найти путь из начального состояния _t_ в самого себя через _t_;
## при помощи решателя ограничений определяется, сколько раз необходимо пройти по второму пути (то есть по циклу), чтобы начать двигаться по первому;
### *TODO: как это делается?*
## построить ограничение в виде композиции действия перехода _t_ и условие срабатывания _t_ и целевого перехода;
## если это ограничение неразрешимо:
### перейти к следующему _t_;
## если это ограничение разрешимо:
### подать полученные значения входных переменных в EFSM;
### последовательно пройти по каждому переходу из найденного алгоритмом Дейкстры пути;
### если условие срабатывания какого-либо из переходов неразрешимо:
#### перейти к следующему _t_.
h2. Литература
*TODO: Дать ссылку на статью.*