Описание асинхронной модели требований

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

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

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

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

Каждому виду взаимодействий ставится в соответствие интерфейсная операция. Для взаимодействий первого типа интерфейсная операция имеет набор входных параметров, описывающих входные данные, и набор выходных параметров, описывающих выходные данные. Такие интерфейсные операции мы будем называть интерфейсными операциями-стимулами. Для взаимодействий второго типа интерфейсная операция имеет только выходные параметры, описывающие выходные данные. Интерфейсные операции такого типа мы будем называть интерфейсными операциями-реакциями.

Для описания требований к поведению целевой системы в рамках асинхронных взаимодействий используется спецификации соответствующих интерфейсных операций. Предусловие операции определяет, какие значения входных параметров являются допустимыми для передачи целевой системе, а постусловие операции определяет какие выходные значения параметров являются корректными для данных значений входных параметров.
Y =

.
Мы будем считать, что каждый элемент дизъюнктивного объединения помечается именем интерфейсного операций и таким образом эти элементы не пересекаются между собой.

множество отложенных реакций Z является дизъюнктивным объединением декартовых произведений множеств допустимых значений выходных параметров всех интерфейсных операций-реакций спецификации
Z =

.
Мы будем считать, что каждый элемент дизъюнктивного объединения помечается именем интерфейсной операции и таким образом эти элементы не пересекаются между собой.

множество переходов E состоит из всех переходов, удовлетворяющих обобщенным предусловию и постусловию спецификации
E = { ( v, ( x, y ), v' )

V x ( (X x Y)

Z ) x V | preS( v, x )

postS( v, x, y, v' ) }

{ ( v, z, v' )

V x ( (X x Y)

Z ) x V | preR( v )

postR( v, z, v' ) },

где предикаты preS =

, postS =

, preR =

, postR =

.

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

---

---