Project

General

Profile

EFSM Traversal » History » Version 11

Igor Melnichenko, 03/11/2014 02:44 PM

1 4 Alexander Kamkin
h1. Обход расширенного конечного автомата (EFSM, Extended Finite State Machine)
2 1 Alexander Kamkin
3 4 Alexander Kamkin
h2. Веронский метод (Franco Fummi et al.)
4 3 Alexander Kamkin
5 4 Alexander Kamkin
Метод обхода EFSM состоит из трёх фаз:
6
# обучение (learning);
7
# случайный обход (random walk);
8
# поиск с возвратами (backjumping).
9
10 1 Alexander Kamkin
h3. Обучение
11
12 5 Alexander Kamkin
В ходе первой фазы анализируются _зависимости_ переходов EFSM по _данным_ и по _управлению_, и строится граф зависимостей — ориентированный граф, вершинами которого являются переходы, а дуги представляют зависимости. Каждая дуга помечается именем переменной и типом зависимости.
13 1 Alexander Kamkin
14 5 Alexander Kamkin
Переход _t_ ~2~ _зависит по данным_ от перехода _t_ ~1~ через переменную _x_, если _t_ ~1~ устанавливает (defines) значение _x_ (действие перехода содержит присваивание в _x_), а _t_ ~2~ использует (uses) _x_ в действии (при вычислении значений внутренних или выходных переменных).
15 4 Alexander Kamkin
16 6 Alexander Kamkin
Переход _t_ ~2~ _зависит по управлению_ от перехода _t_ ~1~ через переменную _x_, если _t_ ~1~ устанавливает (defines) значение _x_, а _t_ ~2~ использует (uses) _x_ в условии срабатывания.
17 4 Alexander Kamkin
18 7 Alexander Kamkin
На этой же фазе происходит выявление переменных-счетчиков и связанных с ними переходов. Переменная _x_ называется _счетчиком_, если существует цикл в графе состояний EFSM, в который входит переход с условием срабатывания, зависящим от _x_, а также переход, в действии которого меняется значение _x_, причем значение _x_ прямо или косвенно зависит от значения _x_.
19 2 Alexander Kamkin
 
20 3 Alexander Kamkin
h3. Случайный обход
21 1 Alexander Kamkin
22 3 Alexander Kamkin
На вход случайного обходчика подаётся два параметра: количество тестовых последовательностей и длина каждой последовательности. В цикле, пока количество тестовых последовательностей не достигнет максимального числа или пока не будут покрыты все переходы выполняются следующие действия:
23
24 1 Alexander Kamkin
# сброс состояния EFSM;
25
# генерация входных векторов в цикле, пока не будет достигнута максимальная длина текущей последовательности.
26
27
Входной вектор генерируется следующим образом:
28
29 9 Igor Melnichenko
# инициализируется пустой входной вектор;
30 1 Alexander Kamkin
# составляется список переходов, исходящих из текущего состояния;
31 9 Igor Melnichenko
# если список не пуст, из него случайным образом выбирается один из переходов (_t_), если пуст — переход на шаг 7;
32
# делается попытка разрешить условие срабатывания _t_;
33 1 Alexander Kamkin
# если условие срабатывания разрешено:
34
## невовлечённым в это условие входным переменным присваиваются случайные значения;
35 9 Igor Melnichenko
## во входной вектор записываются полученные значения входных переменных;
36
## _t_ ставится в соответствие номер текущей последовательности и номер текущего её элемента.
37 8 Igor Melnichenko
# если условие срабатывания не разрешено:
38 9 Igor Melnichenko
## _t_ удаляется из списка;
39
## возврат на шаг 3.
40
# полученный входной вектор подаётся на вход EFSM;
41
# моделируется такт работы EFSM.
42 1 Alexander Kamkin
43 3 Alexander Kamkin
h3. Поиск с возвратами
44 1 Alexander Kamkin
 
45 3 Alexander Kamkin
Составляется список непокрытых переходов, причём переходы, исходящие из посещённых на предыдущем этапе состояний, помещаются в начало списка. Затем циклически выполняются следующие действия:
46 1 Alexander Kamkin
47 10 Igor Melnichenko
# первый переход удаляется из списка и выбирается в качестве целевого;
48
# извлекается сохранённая на предыдущем шаге информация о достижимости начального состояния этого перехода;
49
# на основе этой информации к EFSM применяется соответствующая входная последовательность, и EFSM оказывается в начальном состоянии обрабатываемого перехода;
50
# делается попытка разрешить условие срабатывания этого перехода:
51
# если она успешна, полученный входной вектор добавляется в новую тестовую последовательность, сохраняется информация о достижимости целевого перехода и его обработка заканчивается;
52 3 Alexander Kamkin
# на основании информации о зависимостях по данным извлекаются переходы, которые определяют значение переменных, входящих в условие срабатывания обрабатываемого перехода;
53
# для каждого из них (пусть это будет _t_) выполняются следующие действия:
54 10 Igor Melnichenko
## получить информацию о достижимости начального состояния _t_, выполнить соответствующую тестовую цепочку (если начальное состояние _t_ не было достигнуто ранее, то делается попытка достигнуть его при помощи механизма обратных переходов);
55
## если начальное состояние _t_ недостижимо, перейти к следующему за _t_ элементу списка;
56 3 Alexander Kamkin
## если переход _t_ не обновляет значение счётчика, при помощи алгоритма Дейкстры найти путь от _t_ к целевому переходу;
57
## если в _t_ обновляется значение счётчика, алгоритм Дейкстры применяется два раза: сначала, чтобы найти путь от конечного состояния _t_ до целевого перехода, а затем - чтобы найти путь из начального состояния _t_ в самого себя через _t_;
58 1 Alexander Kamkin
## при помощи решателя ограничений определяется, сколько раз необходимо пройти по второму пути (то есть по циклу), чтобы начать двигаться по первому;
59
## построить ограничение в виде композиции действия перехода _t_ и условие срабатывания _t_ и целевого перехода;
60
## если это ограничение неразрешимо:
61 3 Alexander Kamkin
### перейти к следующему _t_;
62
## если это ограничение разрешимо:
63 1 Alexander Kamkin
### подать полученные значения входных переменных в EFSM;
64 3 Alexander Kamkin
### последовательно пройти по каждому переходу из найденного алгоритмом Дейкстры пути;
65
### если условие срабатывания какого-либо из переходов неразрешимо:
66
#### перейти к следующему _t_.
67 4 Alexander Kamkin
68
h2. Литература
69
70 9 Igor Melnichenko
http://link.springer.com/article/10.1007%2Fs10836-011-5209-8