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



         

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


Для оценки корректности асинхронной модели поведения такую проверку необходимо выполнить для каждой возможной линеаризации мультимножества асинхронных взаимодействий. А в худшем случае число линеаризаций составляет n!, где n - мощность множества P. То есть общая оценка сложности составляет n · n!.

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

Определим для множества P дерево возможных линеаризаций, как дерево, в котором

  • из корня выходит n дуг, из вершин первого уровня - n-1 дуга, …, из вершин n-го уровня - 1 дуга и из вершин n+1-го уровня - ни одной дуги.
  • каждая дуга помечена элементом из P,
  • дуги, выходящие из вершины, путь к которой из корня дерева помечен последовательностью ( p1, p2, …, pk ), помечены элементами P, которые составляют множество Р \ { p1, p2, …, pk }.

Пример дерева возможных линеаризаций для P = { 1, 2, 3 } представлен на рисунке 11.

11.gif

Рисунок 11. Дерево возможных линеаризаций для Р = { 1, 2, 3 }.

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

Припишем к каждой вершине дерева возможных линеаризаций подмножество P, составленное из элементов { p1, p2, …, pk }, которыми помечен путь из корня дерева к данной вершине.

Деревом возможных линеаризаций частично-упорядоченного множества ( P,

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

Идеалами частично-упорядоченного множества ( P,

) называются такие подмножества P, для которых выполнено условие: y
isin.gif I
x
y
x
isin.gif I.

Лемма.

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

) помечены последовательностями элементов из P, составляющими множество всех возможных линеаризаций ( P,
).




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