Модель требований

Абстрактным автоматом будем называть четверку ( V, X, Y, E ), где

V - множество состояний,
X - множество стимулов,
Y - множество реакций,
E
V x X x Y x V - множество переходов.

Переходы автомата ( v, x, y, v' ) состоят из пресостояния v, стимула x, реакции y и постсостояния v'. Множества V, X, Y и E могут быть бесконечными.

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

Моделью требований к целевой системе с интерфейсом ( X, Y, V ) будем называть абстрактный автомат, множества состояний, стимулов и реакций которого совпадают с V, X и Y соответственно.

Будем говорить, что взаимодействие ( v, x, y, v' ) является корректным относительно модели требований A = ( V, X, Y, E ), если оно принадлежит множеству переходов E.

Будем говорить, что модель поведения целевой системы { ( vi, xi, yi, v'i ) } удовлетворяет модели требований A = ( V, X, Y, E ), если

i ( vi, xi, yi, v'i )

Рассмотрим пример с функцией вычисления квадратного корня. Что является моделью требований к этой функции? Интерфейс этой системы ( X, Y, V ) был определен в предыдущем разделе. Множество переходов E определим как все переходы ( ε, x, y, ε )

V x X x Y x V, для которых выполнено следующее ограничение: | x - y2 | < εпогр , где εпогр - некоторое положительное действительное число, меньшее единицы. Тогда взаимодействия ( ε, sqrt( 0.0 ), 0.0, ε ) и ( ε, sqrt( 4.0 ), 2.0, ε ) будут корректными относительно данной модели функциональных требований, а взаимодействие ( ε, sqrt( 10.0 ), 1.0, ε ) - нет.

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

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

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

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

Содержание раздела