Спецификация и тестирование систем с асинхронным интерфейсом

         

Алгоритм проверки корректности поведения - часть 10


  • Алгоритм уменьшает текущий счетчик числа точек ветвления на единицу.

    bound[current]--;

  • Если предыдущая перестановка противоречила частичному порядку
    ;, то алгоритм переходит к шагу 1.

    if (order_failed) goto 1;

  • В противном случае алгоритм вычисляет, не противоречит ли новая перестановка частичному порядку
    , записывает результат в переменную order_failed и переходит к шагу 2, если текущая перестановка не противоречит частичному порядку
    , или к шагу 3 - в противном случае. В последнем случае алгоритм устанавливает значение переменной current равное наименьшему индексу элемента перестановки, для которого нарушается условие линеаризации.

    for(j=current+1;j<=current2;j++) &#x007B;if (order[perm[j],perm[current]]) &#x007B;order_failed = true; goto 3; &#x007D; &#x007D;

    for(j=current+1;j<current2;j++) &#x007B;if (order[perm[current2],perm[j]]) &#x007B;order_failed = true; current = j; goto 3; &#x007D; &#x007D;

    goto 2;

  • Если индекс текущего элемента перестановки равен 0, то алгоритм завершает свою работу с отрицательным вердиктом.

    if (current == 0) КОНЕЦ (асинхронная модель поведения является не корректной относительно данной асинхронной модели требований)

  • В противном случае алгоритм переинициализирует текущий счетчик числа точек ветвления и уменьшает индекс текущего элемента перестановки на единицу.

    bound[current] = n-current; current--;

  • Если индекс текущего элемента перестановки оказался меньше индекса наибольшего элемента пути, содержащего актуальное множество состояний модели требований, то значение последнего устанавливается равным значению первого.

    if (current < processed) processed = current;

  • Алгоритм переходит к шагу 9.

    goto 9;

    Доказательство корректности данного алгоритма представлено в [].

    Частичный порядок

    модели поведения рассматривается в алгоритме в виде двухмерной матрицы n x n, содержащей значение 1 для пар принадлежащих частичному порядку и 0 - в противном случае. Для построения этой матрицы на основе моделей каналов и временных меток можно использовать алгоритм построения транзитивного замыкания Уоршала, который требует O(n3 ) операций [].Существуют также алгоритмы построения транзитивного замыкания с лучшей оценкой (например, O(nlog 7&#x0387;log n)), однако они имеют преимущества только при очень больших значениях n.

    Обратим внимание на тот факт, что оценка сложности алгоритма O(n!) получена для класса детерминированных моделей поведения, для недетерминированных моделей сложность становится еще больше. Но даже при использовании детерминированных моделей требования применимость алгоритма сильно ограничена: при числе взаимодействий, превышающем несколько десятков время работы становится неприемлемо большим. Поэтому при применении рассматриваемого метода необходимо учитывать имеющиеся ограничения на размерность модели поведения, участвующей в задаче оценки корректности.




    Содержание  Назад  Вперед