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



         

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


Алгоритм проверки корректности поведения, представленный ниже, основан на обходе дерева возможных линеаризаций в глубину. В нем используется следующая вспомогательная функция int B (int m , int i ), сложность вычисления которой ограничена константой:

int B(int m, int i) &#x007B; if ((m&#x0025;2 == 0) && (m > 2)) &#x007B;if ( i < m-1 )

return i; else return m-2; &#x007D;

else return m-1; &#x007D;

Сам алгоритм представлен далее.

Алгоритм проверки корректности поведения.

Входные данные.

Асинхронная модель поведения ( P,

) задана:

  • массивом асинхронных взаимодействий P ( &#x007C;P&#x007C; = n );
  • двухмерным массивом частичного порядка order[n,n]
  • order[i,j] = 1, если P[i]
    P[j];
  • order[i,j] = 0, в противном случае.

Асинхронная модель требований A = ( V, X, Y, Z, E ) задана функцией возможных постсостояний &#x03b3; : V x ( (X x Y)

Z )
2V .

Начальное состояние v0

isin.gif V.

Данные алгоритма.

bound : Nat[n] := &#x007B; n, n-1, …, 2, 1 &#x007D;


массив счетчиков числа точек ветвления дерева возможных линеаризаций.

perm : Nat[n] := &#x007B; 0, 1, …, n-1 &#x007D;


       массив, хранящий текущую перестановку взаимодействий.

current : Nat := 0
       индекс текущего элемента перестановки.

path : (V-set)[n+1] := &#x007B; &#x007B;v0&#x007D;, Ø, …, Ø &#x007D;


       массив множеств состояний текущего пути в модели требований. Для детерминированных моделей требований этот массив может быть заменен на массив состояний V, так как все его элементы будут множествами с размерностью не более 1.

processed : Nat := 0
       индекс наибольшего элемента пути, содержащего актуальное множество состояний модели требований.

order_failed : Bool := false
       флаг, содержащий истинное значение только в том случае, когда текущая перестановка не является линеаризацией частичного порядка

.




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