EFSM Traversal » History » Revision 2
Revision 1 (Alexander Kamkin, 02/27/2014 07:45 PM) → Revision 2/13 (Alexander Kamkin, 02/27/2014 07:47 PM)
h1. EFSM Traversal Алгоритм в целом состоит из трёх фаз: # learning; # random randowm walk; # backjumping. 1) В ходе первой фазы они анализируют взаимозависимости переходов по данным и по управлению. Зависимость по данным: один переход устанавливает значение переменной, которую другой переход использует при вычислении значения выхода или другой внутренней переменной. Зависимость по управлению: один переход устанавливает значение переменной, которая входит в условие срабатывания другого перехода. Эти зависимости можно представить в виде направленного графа, в котором узлы — это переходы EFSM, а рёбра представляют зависимости по данным/управлению. Тут же происходит выявление счётчиков и зависимых от них переходов. Переменная x считается счётчиком, если существует такой циклический путь, в который входит переход с гардом зависящим от x, а также переход, в action''е которого меняется значение x, причём значение x прямо или косвенно зависит от предыдущего значения x. 2) На вход случайного обходчика подаётся два параметра: количество тестовых последовательностей и длина одной последовательности. В цикле, пока количество тестовых последовательностей не достигнет максимального числа или пока не будут покрыты все переходы выполняются следующие действия: # сброс состояния EFSM; # генерация входных векторов в цикле, пока не будет достигнута максимальная длина текущей последовательности. Входной вектор генерируется следующим образом: # случайным образом выбирается один из переходов, исходящих из текущего состояния; # делается попытка разрешить его гард; # если гард разрешён, невовлечённым в него входным переменным присваиваются случайные значения, в соответствии с этими значениями обновляется состояние EFSM, сохраняется информация о "достижимости" (выполненному переходу ставится в соответствие номера текущей последовательности и текущего её элемента. 3) составляется упорядоченный список непокрытых переходов, причём переходы, исходящие из уже посещённых на предыдущем этапе состояний помещаются в начало списка. Затем циклически выполняются следующие действия: # выбирается переход из начала списка; # если его гард зависит только от входов EFSM, извлекается сохранённая на предыдущем шаге информация о достижимости начального состояния этого перехода. На основе этой информации к EFSM применяется соответствующая входная последовательность, и EFSM оказывается в состоянии-источнике для обрабатываемого перехода. Разрешается гард этого перехода, переход удаляется из списка; # если его гард зависит не только от входов, извлекается сохранённая на предыдущем шаге информация о достижимости начального состояния этого перехода. На основе этой информации к EFSM применяется соответствующая входная последовательность, и EFSM оказывается в состоянии-источнике для обрабатываемого перехода. Делается попытка разрешить гард этого перехода. Если она успешна, переход удаляется из списка, если нет — обработка продолжается. # на основании информации о зависимостях по данным извлечь переходы, которые определяют значение переменных, входящих в гард обрабатываемого перехода. Для каждого из них (пусть это будет t) выполнить следующие действия: ## получить информацию о достижимости t, выполнить соответствующую тестовую цепочку; ## Если переход t не обновляет значение счётчика, при помощи алгоритма Дейкстры найти путь от t к целевому переходу. Если в t обновляется значение счётчика, алгоритм Дейкстры применяется два раза: сначала, чтобы найти путь от конечного состояния t до целевого перехода, а затем - чтобы найти путь из начального состояния t в самого себя через t. После этого при помощи constraint solver''а определяется, сколько раз необходимо пройти по второму пути (то есть по циклу), чтобы начать двигаться по первому; ## построить constraint в виде композиции action''а перехода t и guard''ов t и целевого перехода; ## если этот constraint неразрешим, перейти к следующему t. Если разрешим, подать полученные значения входов в EFSM, а затем последовательно пройтись по каждому переходу из найденного алгоритмом Дейкстры пути. Если guard какого-либо из переходов оказался невыполнимым, перейти к следующему t.