Project

General

Profile

EFSM Traversal » History » Revision 10

Revision 9 (Igor Melnichenko, 03/01/2014 03:05 PM) → Revision 10/13 (Igor Melnichenko, 03/11/2014 02:19 PM)

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_ называется _счетчиком_, если существует цикл в графе состояний EFSM, в который входит переход с условием срабатывания, зависящим от _x_, а также переход, в действии которого меняется значение _x_, причем значение _x_ прямо или косвенно зависит от значения _x_. 
 
 h3. Случайный обход 

 На вход случайного обходчика подаётся два параметра: количество тестовых последовательностей и длина каждой последовательности. В цикле, пока количество тестовых последовательностей не достигнет максимального числа или пока не будут покрыты все переходы выполняются следующие действия: 

 # сброс состояния EFSM; 
 # генерация входных векторов в цикле, пока не будет достигнута максимальная длина текущей последовательности. 

 Входной вектор генерируется следующим образом: 

 # инициализируется пустой входной вектор; 
 # составляется список переходов, исходящих из текущего состояния; 
 # если список не пуст, из него случайным образом выбирается один из переходов (_t_), если пуст — переход на шаг 7; 
 # делается попытка разрешить условие срабатывания _t_; 
 # если условие срабатывания разрешено: 
 ## невовлечённым в это условие входным переменным присваиваются случайные значения; 
 ## во входной вектор записываются полученные значения входных переменных; 
 ## _t_ ставится в соответствие номер текущей последовательности и номер текущего её элемента. 
 # если условие срабатывания не разрешено: 
 ## _t_ удаляется из списка; 
 ## возврат на шаг 3. 
 # полученный входной вектор подаётся на вход EFSM; 
 # моделируется такт работы EFSM. 

 h3. Поиск с возвратами 
 
 Составляется список непокрытых переходов, причём переходы, исходящие из посещённых на предыдущем этапе состояний, помещаются в начало списка. Затем циклически выполняются следующие действия: 

 # первый выбирается переход удаляется из списка начала списка; 
 # если его условие срабатывания зависит только от входных переменных: 
 ## извлекается сохранённая на предыдущем шаге информация о достижимости начального состояния этого перехода; 
 ## на основе этой информации к EFSM применяется соответствующая входная последовательность, и выбирается EFSM оказывается в качестве целевого; начальном состоянии обрабатываемого перехода; 
 ## разрешается условие срабатывания этого перехода; 
 ### *TODO: А если условие неразрешимо?* 
 ## переход удаляется из списка; 
 # если его условие срабатывания зависит не только от входных переменных: 
 ## извлекается сохранённая на предыдущем шаге информация о достижимости начального состояния этого перехода; 
 # ## на основе этой информации к EFSM применяется соответствующая входная последовательность, и EFSM оказывается в начальном состоянии обрабатываемого перехода; 
 # ## делается попытка разрешить условие срабатывания этого перехода: 
 # ### если она успешна, полученный входной вектор добавляется в новую тестовую последовательность, сохраняется информация о достижимости целевого перехода и его переход удаляется из списка; 
 ### если нет — обработка заканчивается; продолжается; 
 # на основании информации о зависимостях по данным извлекаются переходы, которые определяют значение переменных, входящих в условие срабатывания обрабатываемого перехода; 
 # для каждого из них (пусть это будет _t_) выполняются следующие действия: 
 ## получить информацию о достижимости начального состояния _t_, выполнить соответствующую тестовую цепочку (если начальное состояние _t_ не было достигнуто ранее, то делается попытка достигнуть его при помощи механизма обратных переходов); цепочку; 
 ## ### *TODO: что делать, если начальное состояние _t_ недостижимо, перейти к следующему за _t_ элементу списка; недостижимо?* 
 ## если переход _t_ не обновляет значение счётчика, при помощи алгоритма Дейкстры найти путь от _t_ к целевому переходу; 
 ## если в _t_ обновляется значение счётчика, алгоритм Дейкстры применяется два раза: сначала, чтобы найти путь от конечного состояния _t_ до целевого перехода, а затем - чтобы найти путь из начального состояния _t_ в самого себя через _t_; 
 ## при помощи решателя ограничений определяется, сколько раз необходимо пройти по второму пути (то есть по циклу), чтобы начать двигаться по первому; 
 ### *TODO: как это делается?* 
 ## построить ограничение в виде композиции действия перехода _t_ и условие срабатывания _t_ и целевого перехода; 
 ## если это ограничение неразрешимо: 
 ### перейти к следующему _t_; 
 ## если это ограничение разрешимо: 
 ### подать полученные значения входных переменных в EFSM; 
 ### последовательно пройти по каждому переходу из найденного алгоритмом Дейкстры пути; 
 ### если условие срабатывания какого-либо из переходов неразрешимо: 
 #### перейти к следующему _t_. 

 h2. Литература 

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