Модель временных меток

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

Пусть ( TM,

TM ) - частично-упорядоченное множество временных меток. Тогда временным интервалом мы будем называть пару временных меток ( tm1, tm2 ), в которой вторая метка больше либо равна первой (т.е. tm1 = tm2 tm1 TM tm2).

Множество всех временных интервалов будет обозначаться TI(TM). Определим на нем частичный порядок

TI следующим образом:

( tm1, tm2 )

TI ( tm'1, tm'2 ) tm2 TM tm'1

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

Пусть D - конечное или бесконечное множество, а ( TM,

TM ) - множество временных меток. Тогда моделью временных меток на множестве D мы будем называть отображение τ : D TI(TM).

Модель временных меток задает на множестве D частичный порядок

τ :

d1

τ d2 τ(d1) TI τ(d2).

В качестве множества временных меток TM в технологии UniTesK используется множество (F x Nat)

{ -∞, +∞ }, где F - конечное или бесконечное множество систем координат, Nat - множество натуральных чисел, а -∞ и +∞ - специально выделенные значения.

Для описания частичного порядка

TM применяются следующие правила:

• 
  f
  
  F
  
  n
  
  Nat-∞
  
  TM ( f, n ),
• 
  f
  
  F
  
  n
  
  Nat     ( f, n )
  
  TM +∞,
• 
  f
  
  F
  
  n1,n2
  
  Nat n1 < n2
  
  ( f, n1 )
  
  TM ( f, n2 ),
• 
  f1,f2
  
  F
  
  n1,n2
  
  Nat ( f1, n1 )
  
  TM ( f2, n2 ), если эта зависимость была зафиксирована разработчиком теста и она не противоречит определению частичного порядка (иррефлексивность, антисимметричность и транзитивность).

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

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

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

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

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

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

---

---