Project

General

Profile

EFSM Traversal » History » Version 1

Alexander Kamkin, 02/27/2014 07:45 PM

1 1 Alexander Kamkin
h1. EFSM Traversal
2
3
Алгоритм в целом состоит из трёх фаз:
4
# learning;
5
# randowm walk;
6
# backjumping.
7
 
8
1) В ходе первой фазы они анализируют взаимозависимости переходов по данным и по управлению. Зависимость по данным: один переход устанавливает значение переменной, которую другой переход использует при вычислении значения выхода или другой внутренней переменной. Зависимость по управлению: один переход устанавливает значение переменной, которая входит в условие срабатывания другого перехода.
9
Эти зависимости можно представить в виде направленного графа, в котором узлы — это переходы EFSM, а рёбра представляют зависимости по данным/управлению.
10
Тут же происходит выявление счётчиков и зависимых от них переходов. Переменная x считается счётчиком, если существует такой циклический путь, в который входит переход с гардом зависящим от x, а также переход, в action''е которого меняется значение x, причём значение x прямо или косвенно зависит от предыдущего значения x.
11
 
12
2) На вход случайного обходчика подаётся два параметра: количество тестовых последовательностей и длина одной последовательности.
13
В цикле, пока количество тестовых последовательностей не достигнет максимального числа или пока не будут покрыты все переходы выполняются следующие действия:
14
15
    сброс состояния EFSM;
16
    генерация входных векторов в цикле, пока не будет достигнута максимальная длина текущей последовательности.
17
18
Входной вектор генерируется следующим образом:
19
20
    случайным образом выбирается один из переходов, исходящих из текущего состояния;
21
    делается попытка разрешить его гард;
22
    если гард разрешён, невовлечённым в него входным переменным присваиваются случайные значения, в соответствии с этими значениями обновляется состояние EFSM, сохраняется информация о "достижимости" (выполненному переходу ставится в соответствие номера текущей последовательности и текущего её элемента.
23
24
 
25
3) составляется упорядоченный список непокрытых переходов, причём переходы, исходящие из уже посещённых на предыдущем этапе состояний помещаются в начало списка. Затем циклически выполняются следующие действия:
26
27
    выбирается переход из начала списка;
28
    если его гард зависит только от входов EFSM, извлекается сохранённая на предыдущем шаге информация о достижимости начального состояния этого перехода. На основе этой информации к EFSM применяется соответствующая входная последовательность, и EFSM оказывается в состоянии-источнике для обрабатываемого перехода. Разрешается гард этого перехода, переход удаляется из списка;
29
    если его гард зависит не только от входов, извлекается сохранённая на предыдущем шаге информация о достижимости начального состояния этого перехода. На основе этой информации к EFSM применяется соответствующая входная последовательность, и EFSM оказывается в состоянии-источнике для обрабатываемого перехода. Делается попытка разрешить гард этого перехода. Если она успешна, переход удаляется из списка, если нет — обработка продолжается.
30
    на основании информации о зависимостях по данным извлечь переходы, которые определяют значение переменных, входящих в гард обрабатываемого перехода. Для каждого из них (пусть это будет t) выполнить следующие действия:
31
32
    получить информацию о достижимости t, выполнить соответствующую тестовую цепочку;
33
    Если переход t не обновляет значение счётчика, при помощи алгоритма Дейкстры найти путь от t к целевому переходу. Если в t обновляется значение счётчика, алгоритм Дейкстры применяется два раза: сначала, чтобы найти путь от конечного состояния t до целевого перехода, а затем - чтобы найти путь из начального состояния t в самого себя через t. После этого при помощи constraint solver''а определяется, сколько раз необходимо пройти по второму пути (то есть по циклу), чтобы начать двигаться по первому;
34
    построить constraint в виде композиции action''а перехода t и guard''ов t и целевого перехода;
35
    если этот constraint неразрешим, перейти к следующему t. Если разрешим, подать полученные значения входов в EFSM, а затем последовательно пройтись по каждому переходу из найденного алгоритмом Дейкстры пути. Если guard какого-либо из переходов оказался невыполнимым, перейти к следующему t.