ПРОГРАММИРОВАНИЕ, 2011, No 1, с. 3-19
ТЕСТИРОВАНИЕ, ВЕРИФИКАЦИЯ И ВАЛИДАЦИЯ ПРОГРАММ =
УДК 681.3.06
ПОПОЛНЕНИЕ СПЕЦИФИКАЦИИ ДЛЯ IOCO
© 2011 г. И. Б. Бурдонов, А. С. Косачев
Институт системного программирования РАН
109004 Москва, ул. Александра Солженицына, 25 E-mail: {igor,kos} @ispras.ru Поступила в редакцию 18.07.2010 г.
Статья посвящена проблемам отношения ioco, определяющего соответствие (конформность) реализации спецификации. Рассматриваются проблемы нерефлексивности отношения ioco, наличие в спецификации неконформных (отсутствующих в любой конформной реализации) трасс, несохранение ioco при композиции (композиция реализаций, конформных своим спецификациям, может быть неконформна композиции этих спецификаций) и проблема "ложных" ошибок при тестировании в контексте. Для решения этих проблем в статье предлагается алгоритм пополнения спецификации, по отношению к которому ioco инвариантно (сохраняется класс конформных реализаций). На классе пополненных спецификаций указанные проблемы отсутствуют.
1. ВВЕДЕНИЕ
Правильность исследуемой системы понимается как её соответствие (конформность) заданным требованиям. Когда говорят о верификации конформности на основе формальных моделей, то предполагают, что система отображается в реализационную модель (реализацию), требования - в спецификационную модель (спецификацию), а их соответствие - в бинарное отношение конформности. Если требования к системе выражаются в терминах ее взаимодействия с внешним окружением, то соответствующую конформность можно проверять с помощью тестирования, то есть в процессе тестовых экспериментов над исследуемой системой.
Одной из наиболее известных конформностей является отношение ioco (Input-Output Conformance), предложенное Яном Тритмансом [12]. Взаимодействие понимается как обмен дискретными порциями информации между реализацией и окружением. То, что передается из окружения в реализацию, называется стимулом (input), а то, что реализация передает в окружение, - реакцией (output). Предполагается, что в реализации не может возникнуть отказ от приема стимула (блокировка стимула), однако реализация может отказаться выдавать реакции, причем такой отказ составляет особый тип наблюдения
за поведением реализации, обозначаемый символом 5. Результатом тестового эксперимента является трасса наблюдений - последовательность стимулов, реакций и отказов 5.
Отношение ioco определяется на моделях, которыми являются системы помеченных переходов (LTS - Labelled Transition System). LTS основана на понятиях состояния и перехода между состояниями трех видов: переход по стимулу, переход по реакции и внутренний, ненаблюдаемый т -переход.
Отношение ioco предполагает, что реализация всегда готова принять любой стимул (всюду определена по стимулам), тогда как на спецификацию такого ограничения не налагается. Это различие приводит к проблеме нерефлексивности отношения ioco. Как следствие, в спецификации могут быть неконформные трассы, которых не может быть ни в какой конформной реализации.
Кроме этого, в ioco-реализации и ioco-специ-фикации не должно быть бесконечных цепочек т-переходов (дивергенции). Это приводит к некоторым проблемам при композиции таких моделей, поскольку в результате композиции дивергенция может возникнуть.
С композицией связана и основная проблема отношения ioco - нарушение монотонности: несохранение конформности при композиции, когда композиция реализаций, конформных своим
спецификациям, оказывается неконформной композиции этих спецификаций. Особая разновидность проблемы монотонности проявляется при тестировании в контексте, когда тест взаимодействует с реализацией не напрямую, а через некоторый контекст (например, очереди стимулов и/или реакций). Композиция конформной реализации с контекстом может оказаться неконформна композиции спецификации с этим контекстом. В результате тест ловит "ложные" ошибки, которых не бывает при непосредственном взаимодействии теста с реализацией.
Для решения указанных проблем обычно предлагается то или иное преобразование спецификации, называемое пополнением [3,6,7,8,10,13,14]. Пополненные спецификации всюду определены по стимулам так же, как реализации, и указанные выше проблемы отсутствуют или значительно ослабляются на классе таких спецификаций. Однако, существенный недостаток предлагавшихся до сих пор преобразований заключается в том, что по отношению к ним не инвариантно само отношение ioco: в результате пополнения конформность может ослабляться (некоторые неконформные реализации становятся конформными) и/или усиливаться (некоторые конформные реализации становятся неконформными) [1, раздел 2.5.3].
Наилучшим можно считать так называемое демоническое пополнение (demonic completion) [13,14], при котором блокировка стимулов стимула заменяется на так называемое хаотическое поведение [4], допускающее любые трассы наблюдений. Это пополнение не усиливает конформность, но может ее ослабить. В [7] предлагается пополнение, которое лишено указанных недостатков, но, во-первых, оно определяется не для отношения ioco, а для более простого отношения ioconf, и, во-вторых, преобразуется не LTS, а множество ее трасс, то есть не строится LTS с пополненным множеством трасс, что не дает возможности использовать такое пополнение при композиции LTS-моделей.
Предлагавшиеся ранее пополнения не решают проблему "ложных" ошибок при тестировании в контексте общего вида, в котором допускаются блокировки стимулов. Заметим, что такие контексты встречаются на практике. Например, ограниченные очереди стимулов и реакций можно трактовать как LTS с блокировкой стимулов (когда очередь полна).
В данной статье предлагаются два преобра-
зования пополнения LTS-спецификаций, которые лишены указанных недостатков и применяются для ограниченных, но достаточно широких классов спецификаций. Первое преобразование применяется тогда, когда не предполагается тестирование в контексте, который не всюду определен по стимулам. Второе, более сложное, преобразование налагает на спецификации более сильные ограничения, но может применяться во всех случаях.
Во 2-ом разделе статьи вводятся основные понятия и обозначения LTS, определяются отношение ioco, композиция LTS и генерация тестов для ioco. В 3-ем разделе более подробно рассматривается проблематика отношения ioco, приводятся примеры спецификаций и реализаций, на которых демонстрируются рассматриваемые проблемы. В разделе 4 определяется первое из предлагаемых пополнений LTS-спецификаций, которое в 5-ом разделе демонстрируется на примерах из раздела 3. В 6-ом разделе определяется второе преобразование для тестирования в контексте общего вида.
2. LTS-МОДЕЛЬ И ОТНОШЕНИЕ IOCO
2.1. Система помеченных переходов (LTS)
В качестве модели реализации и спецификации используется LTS (Labelled Transition System), определяемая как совокупность S = LTS(VS,L,Es, so), где Vs - непустое множество состояний, L - алфавит внешних действий, ES С VS х (L U {т}) х VS - множество переходов, so € Vs - начальное состояние. Класс всех LTS обозначим LTS. Для LTSi С LTS класс всех LTS в алфавите L, принадлежащих LTSi, будем обозначать LTSi(L).
Одинарными стрелками обозначаются наличие/отсутствие переходов:
u / Д 1 1\ - -л s—hs' = (s, u, s') € ES,
U Д -h ' u ' s^ = js's—s'.
Последовательность внешних действий называется трассой. Для данного состояния s говорят о трассах, начинающихся в этом состоянии, и о состояниях, в которых такие трассы заканчиваются.
Формально для z €L и а = (zi,..., zn) €L*
/ Д /
s^s' = s = s'
w"l T T T '
Vds1, . . . , sn s = s1—s2—. . .—sn = s',
<z> ' Д -, z '
s=^s' = ds1,s2 s^s1— s2 ^s',
а , А -,
S^S = dSö, . . . , Sn
(Zi) (zn) '
S = So =^Si . . . Sn-1 Sn = S', а А -, ' а ' S=^ = zis' S=^S
s after a = {s'|s=W}.
Состояние s достижимо, если в него можно попасть из начального состояния по некоторой трассе. Множество достижимых состояний LTS S будем обозначать
der(S) = {s € Vs|Za So=^s}. Состояние s терминальное, если из него не выходят никакие переходы: Vu € L U {т} S— . Состояние s стабильное, если из него не выходят т-переходы: s -— . Состояние s дивергентное (обозначается s если в нем начинается бесконечная цепочка т-переходов. В противном случае состояние s конвергентно. LTS строго кон-вергентна, если в ней все достижимые состояния конвергентны. Класс всех строго конвергентных LTS обозначим LTSi.
2.2. ioco-семантика взаимодействия
В семантике отношения ioco предполагается, что универсум внешних действий L разбит на универсум стимулов (input) X и универсум реакций (output) Y: L = X U Y & X П Y = 0. Для алфавита LTS L С L обозначим X = L П X и
Y = L П Y. Тогда L = X U Y & X П Y = 0. Взаимодействие реализации в алфавите L С L с окружением сводится к последовательности актов взаимодействия двух типов: 1) посылка одного указанного стимула x € X из окружения в реализацию и 2) прием любой реакции y €
Y из реализации в окружение. Предполагается, что в реализации не может возникнуть отказ (refusal) от приема стимула, называемый блокировкой стимула. В то же время реализация может отказаться выдавать реакции, причем этот отказ наблюдаем, и такое наблюдение обозначается символом ö.
Состояние s будем называть стационарным (quiescent) и обозначать ö(s), если оно стабильно и в нем не определены переходы по реакциям:
ö(s) = Vu € Y U {т} s —. Отказ ö наблюдается в стационарных состояниях реализации. Добавим в стационарных состояниях LTS S переходы-петли по символу ö: S-—s = ö(s). Тем самым, мы получим новую LTS S' = LTS(Vs, Ls, Es', s0), где Ls = LU{ö} и Es' = Esu{(s,ö,s)|s€Vs & ö(s)}. Будем называть S-трассой (suspension trace) LTS S трассу LTS S' и распространим на S-трассы
обозначения с двойной стрелкой. Обозначим множество S-трасс LTS S: Straces(S) А {ö€L||so=^}.
LTS в алфавите X U Y называется всюду определенной по стимулам, если в каждом ее достижимом стабильном состоянии определены переходы по всем стимулам: Vs € der (S)(s— ^ Vx € X s—).
Спецификацией для ioco будем считать строго конвергентную LTS в алфавите L С L. Реализацией для ioco будем считать строго конвергентную LTS в алфа
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.