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



         

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


Предположим, что нам даны конечная асинхронная модель поведения целевой системы ( P,

) и асинхронная модель требований A = ( V, X, Y, Z, E ) с начальным состоянием v0
isin.gif V. Как проверить, находятся ли эти модели в отношении "удовлетворяет" или нет?

Для этого необходимо проверить существование пути ( e1, e2, …, en ) в автомате A, начинающегося в состоянии v0 и помеченного взаимодействиями из P так, чтобы это не противоречило частичному порядку π.

Асинхронная модель требований A = ( V, X, Y, Z, E ) задается асинхронной спецификацией { SpecSi | i = 1, …, k; k > 0 }

{ SpecRj | j = 1, …, m; m ≥ 0 }, которая определяет переходы автомата неявным образом. Это осложняет решение поставленной задачи, так как вычисление состояний, в которые можно попасть из данного состояния по переходам помеченным данным символом, сводится к решению системы уравнений.

В данном разделе мы не будем рассматривать пути решения этой проблемы. Здесь мы будем считать, что нам задана вспомогательная функция γ : V x ( (X x Y)

Z )
2V , вычисляющая множество состояний, которые модель требований допускает в качестве постсостояния перехода с данным пресостоянием v и асинхронным взаимодействием p:

γ( v, p ) = { v'

isin.gif V | ( v, p, v' )
isin.gif E }

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

Определение 12.

Линейный порядок < на частично-упорядоченном множестве ( P,

) называется линеаризацией, если он сохраняет частичный порядок
, то есть

p1, p2
isin.gif P p1
p2
p1 < p2.

Для последующего рассмотрения введем вспомогательную функцию Г*, вычисляющую по состоянию в автомате и последовательности асинхронных взаимодействий, множество состояний автомата, достижимых из данного по последовательности дуг, помеченных данной последовательностью взаимодействий.


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