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



         

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


Формальное определение функции Г* следующее:

Г* ( v0, ( p1, p2, …, pn ) ) =

image070.gif
, где

Г( V, p ) =

image072.gif
.

Лемма.

Для последовательности асинхронных взаимодействий ( p1, p2, …, pn ) существует путь ( e1, e2, …, en ) в автомате A, начинающийся в состоянии v0 и помеченный данными взаимодействиями, тогда и только тогда, когда Г* ( v0, ( p1, p2, …, pn ) ) ≠ Ø.

Доказательство.

Действительно, пусть существует путь v0

image074.gif
v1
image076.gif
image078.gif
vn в автомате A, начинающийся в состоянии v0 и помеченный взаимодействиями ( p1, p2, …, pn ). Докажем индукцией по длине пути, что vn
isin.gif Г*( v0, ( p1, p2, …, pn ) ), а следовательно Г* ( v0, ( p1, p2, …, pn ) ) ≠ Ø.

Базис индукции. (n = 1)

Итак, пусть v0

image074.gif
v1. Тогда v1
isin.gif γ( v0, p1 )
v1
isin.gif Г( {v0}, p1 ) = Г*( v0, ( p1 ) ).

Шаг индукции.

Предположим, что мы доказали утверждение для путей длины n-1. Докажем его для n.

Пусть существует путь v0

image074.gif
v1
image076.gif
image078.gif
vn в автомате A, начинающийся в состоянии v0 и помеченный взаимодействиями ( p1, p2, …, pn ). Тогда по предположению индукции vn-1
isin.gif Г*( v0, ( p1, p2, …, pn-1 ) ). Но vn-1
image078.gif
vn, то есть vn
isin.gif γ( vn-1, pn )
vn
isin.gif Г( Vn-1, pn ), где Vn-1 - любое множество, содержащее vn-1, в том числе Vn-1 = Г*( v0, ( p1, p2, …, pn-1 ) ). Следовательно vn
isin.gif Г( Г*( v0, ( p1, p2, …, pn-1 ) ), pn ) = Г*( v0, ( p1, p2, …, pn ) ).

В обратную сторону.

Пусть Г*( v0, ( p1, p2, …, pn ) ) ≠ Ø. Докажем индукцией по n, что в автомате A существует путь v0

image074.gif
v1
image076.gif
image078.gif
vn, начинающийся в состоянии v0 и помеченный взаимодействиями ( p1, p2, …, pn ).

Базис индукции. (n = 1)

Пусть Г* ( v0, ( p1 ) ) ≠ Ø. Тогда существует v1

isin.gif Г* ( v0, ( p1 ) ) = Г( {v0}, p1 ) = γ( v0, p1 ). То есть переход v0
image074.gif
v1 принадлежит автомату A и является искомым путем.

Шаг индукции.

Предположим, что мы доказали утверждение для n-1. Докажем его для n.

Пусть Г* ( v0, ( p1, p2, …, pn ) ) ≠ Ø.

Тогда

k
isin.gif {1,…,n-1}
vk
isin.gif Г* ( v0, ( p1, p2, …, pk ) ): Г* ( vk, ( pk+1, pk+2, …, pn ) ) ≠ Ø.




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