Об одном классе базовых протоколов
Рассматривается проблема представления требований к поведению интерактивной системы в виде формальных спецификаций, а также ее верификация и генерация трасс, используемых для создания тестовых наборов. Исследуется специальный класс спецификаций, представленный в виде базовых протоколов, в котором ра...
Saved in:
| Date: | 2005 |
|---|---|
| Main Author: | |
| Format: | Article |
| Language: | Russian |
| Published: |
Інститут програмних систем НАН України
2005
|
| Subjects: | |
| Online Access: | https://nasplib.isofts.kiev.ua/handle/123456789/1318 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Journal Title: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Cite this: | Об одном классе базовых протоколов / А.А.Летичевский // Проблеми програмування. — 2005. — N 4. — С. 3-19. — Бібліогр.: 7 назв. — рос. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1859744164586979328 |
|---|---|
| author | Летичевский, А.А. |
| author_facet | Летичевский, А.А. |
| citation_txt | Об одном классе базовых протоколов / А.А.Летичевский // Проблеми програмування. — 2005. — N 4. — С. 3-19. — Бібліогр.: 7 назв. — рос. |
| collection | DSpace DC |
| description | Рассматривается проблема представления требований к поведению интерактивной системы в виде формальных спецификаций, а также ее верификация и генерация трасс, используемых для создания тестовых наборов. Исследуется специальный класс спецификаций, представленный в виде базовых протоколов, в котором рассматриваются возможные виды противоречивости и неполноты. С помощью символьного моделирования требований, производится порождение символьных трасс, используемых для тестирования создаваемой системы по различными критериями.
|
| first_indexed | 2025-12-01T19:47:37Z |
| format | Article |
| fulltext |
Методи і засоби програмної інженерії
© А.А. Летичевский, 2005
ISSN 1727-4907. Проблеми програмування. 2005. № 4 3
УДК 623/518.3/517.5
А.А.Летичевский
ОБ ОДНОМ КЛАССЕ БАЗОВЫХ ПРОТОКОЛОВ
Рассматривается проблема представления требований к поведению интерактивной системы в виде
формальных спецификаций, а также ее верификация и генерация трасс, используемых для создания
тестовых наборов. Исследуется специальный класс спецификаций, представленный в виде базовых про-
токолов, в котором рассматриваются возможные виды противоречивости и неполноты. С помощью
символьного моделирования требований, производится порождение символьных трасс, используемых
для тестирования создаваемой системы по различными критериями.
1. Проблема верификации и форма-
лизации требований
Сбор требований является началь-
ным и неотъемлемым этапом процесса раз-
работки и заключается в определении на-
бора функциональностей, который необхо-
димо реализовать в продукте. Процесс
сбора реализуется частично в общении с за-
казчиком, частично посредством мозговых
штурмов разработчиков. Результатом явля-
ется формирование набора требований к
системе, именуемой в отечественной прак-
тике техническим заданием.
Фиксация требований (Requirement
Capturing), с одной стороны, определяется
желаниями заказчика в реализации того или
иного свойства. С другой стороны, в про-
цессе сбора требований может обнару-
житься ошибка, которая приведет к опре-
деленным последствиям, устранение кото-
рых потребует дополнительное кодирова-
ние, редизайн, перепланирование и др.
Ошибка может быть тем серьезней,
чем позже она будет обнаружена, особенно
если это связано с сотнями и тысячами спе-
цификаций, например в описании телеком-
муникационных протоколов или описании
работы операционной системы.
Поэтому одной из составляющей
этапа фиксации требований наряду со сбо-
ром является верификация требований, а
именно проверка их на непротиворечивость
и полноту.
Автоматизированная верификация
требований может проводиться лишь после
формального описания или формализации
требований.
Формализация включает в себя опре-
деление компонентов системы и их состоя-
ний, сигналов, с помощью которых взаимо-
действуют компоненты, и условий в фор-
мальном виде, которые должны выпол-
няться при изменении состояний компонен-
тов. Для формального описания поведения
системы используются языки инженерных
спецификаций MSC [1], SDL [2], UML [3]. В
[4-6] в качестве формальной модели для
описания требований использовалось поня-
тие системы базовых протоколов. Описание
систем с помощью базовых протоколов до-
полняет языки инженерных спецификаций,
поднимая уровень абстракции и позволяя
использовать дедуктивные средства вери-
фикации в сочетании с моделированием
поведения систем путем генерации трасс и
проверки моделей, извлекаемых из базовых
протоколов. Совокупность сгенерирован-
ных трасс является основой для создания
множества тестов, которые впоследствии
будут использованы для тестирования раз-
работанного продукта. Возможен также
синтез модели продукта по формализован-
ным требованиям на том уровне абстрак-
ции, на котором описаны требования с ис-
пользованием средств языков MSC и SDL.
Эта модель может быть основой для даль-
нейшей разработки продукта.
В данной статье рассматривается
специальный класс базовых протоколов, на-
зываемых К-протоколами и определяемых
как асинхронные императивные протоколы
с одним ключевым агентом. Для этого
класса протоколов строятся специальные
алгоритмы верификации, генерации трасс и
тестовых последовательностей, более эф-
фективные, чем для базовых протоколов
общего вида. Несмотря на строгие ограни-
чения, К-протоколы часто встречаются на
практике в таких областях, как телекомму-
никации, телематика и др.
Методи і засоби програмної інженерії
4
2. Базовые протоколы
Базовый протокол является фор-
мальной записью утверждения о некоторых
событиях, которые должны произойти в
программе, алгоритме, протоколе при вы-
полнении определенных условий. Напри-
мер, в утверждении “Если после набора
номера телефон получает сигнал dial_busy,
он переходит в состояние занято” присут-
ствуют три компонента: предусловие –
«После набора номера», процесс – «Получе-
ние сигнала dial_busy» и постусловие – «Со-
стояние занято».
Базовый протокол имеет вид анало-
гичный тройке Хоара βα >→< P , α и β
называются предусловием и постусловием
соответственно, а Р – процессом протокола.
Условия α и β представляются с помощью
логических выражений некоторого базового
языка и определяют условия на множестве
состояний системы. Рассматриваются также
параметризованные протоколы, имеющие
вид )( βα >→<∀ Px , где x – список пара-
метров протокола, а формулы α и β вместе с
процессом P могут зависеть от этих пара-
метров.
Общая теория базовых протоколов
изложена в [4]. Она содержит общее опре-
деление систем базовых протоколов, их се-
мантику и различение конкретных и абст-
рактных протоколов, а также связей между
ними. Первые используются для точного
моделирования поведения систем, вторые –
для распознавания их свойств с использова-
нием дедуктивных средств.
В данной статье рассмотрим класс
базовых протоколов, который является ча-
стным случаем конкретных базовых про-
токолов из [4]. Этот класс можно опреде-
лить как класс асинхронных императивных
базовых протоколов с одним ключевым
агентом. Базовые протоколы указанного
класса будем называть К-протоколами.
Асинхронность понимается в том смысле,
что обмен информацией осуществляется по
буферизованным каналам. Императивность
означает, что каждый протокол эквивален-
тен некоторой императивной программе, а
один ключевой агент полностью определяет
функционирование базового протокола. Бо-
лее точные определения следуют ниже.
Система, определяемая базовыми
протоколами, представляется в виде ком-
позиции среды и агентов, которые в нее по-
гружены [7]. Состояние среды формируется
набором значений атрибутов среды, иг-
рающих роль общей памяти и параметров
(атрибутов) агентов. Совокупность атри-
бутов агента образует его локальную па-
мять. Агенты имеют типы и имена, а также
могут находиться в конкретных состояниях.
Состояние агента однозначно устанавливает
поведение системы после погружения в нее
агента в данном состоянии. Функция по-
гружения определяется как параллельное
погружение, т.е. ]||[],[ vusvus = , где vu ||
обозначает параллельную асинхронную
композицию агентов (интерливинг). Приме-
ром среды является телефонная сеть.
Агенты – это телефоны, а их параметры
включают в себя номера телефонов, ре-
жимы подключения, отношения с другими
телефонами (например, соединение) и дру-
гие характеристики, изменяющиеся во вре-
мени.
Атрибуты среды и параметры аген-
тов имеют типы: арифметический, логиче-
ский (булевский) и символьный. Арифме-
тические типы делятся на целые и вещест-
венные, а символьные представляются ал-
гебраическими выражениями в заданной
сигнатуре и могут быть определены как аб-
страктные типы данных путем задания ре-
дукций (переписывающих правил, опреде-
ляющих каноническую форму). Параметр p
агента a типа T записывается в виде T a.P.
Набор параметров агента однозначно опре-
деляется его типом. Утверждение о том, что
агент a типа T находится в состоянии u, за-
писывается в виде T(a,u).
Агенты взаимодействуют между со-
бой путем асинхронного обмена сообще-
ниями. Передача сообщения представляется
действием
)),...,(, , ( 1 mppxaTaT ′′Out ,
где а – имя передающего агента типа Т; a′ –
имя агента типа T ′ , которому передается
сообщение x; mpp ,...,1 – параметры сообще-
ния (выражения в языке данных). По-
скольку имена агентов уникальны, то указа-
тель типа в них может отсутствовать. Пред-
полагается, что каждый агент имеет вход-
Методи і засоби програмної інженерії
5
ную очередь поступающих к нему сообще-
ний. Прием осуществляется путем чтения
первого сообщения из очереди, а передача
ставит сообщение в конец соответствующей
очереди. Различаем внешние (наблюдае-
мые) и внутренние действия, выполняемые
агентами. Передача сообщений относится к
наблюдаемым действиям и входит в про-
цесс базового протокола. Что же касается
приема, то это внутреннее действие, выпол-
няемое неявно, при обращении к первому
элементу очереди. Это обращение осущест-
вляется при проверке истинности предиката
), ( zaTIn , используемого в предусловиях. В
предикате z есть выражение, которое может
зависеть от переменных (параметров прото-
кола). Предикат имеет значение истина,
если очередь входных сообщений не пуста,
и первое в очереди сообщение сопоставля-
ется с выражением z (мэтчинг). Для опре-
деления того, что очередь пуста, использу-
ется предикат emptyq(n), который прини-
мает значение 1, если в очереди нет сооб-
щений.
Кроме действий, выражающих прием
и передачу сообщений, агенты могут вы-
полнять наблюдаемые локальные действия,
обозначаемые как action X, где X – имя ло-
кального действия. Результат выполнения
локального действия определяется посту-
словием.
Рассмотрим дополнительные ограни-
чения на базовые протоколы. Предусловие
ограниченного протокола b имеет вид
FuaTb ∧= ),()(pred , где а – имя ключевого
агента типа Т, участвующего в протоколе; u
– его состояние; F – логическое выражение,
построенное с помощью логических связок,
равенств и неравенств из атрибутов среды и
параметров ключевого агента. Процесс
proc(b) протокола b представляет собой
последовательность maaa .. .21 действий, вы-
полняемых ключевым агентом. Все эле-
менты этой последовательности представ-
ляют собой передачи сообщений от ключе-
вого агента другим агентам и локальные
действия. В случае, когда порядок выполне-
ния некоторых действий не существен, вме-
сто последовательности могут рассматри-
ваться выражения алгебры процессов с не-
детерминированным выбором. Постусло-
вие post(b) базового протокола b представ-
ляет собой конъюнкцию
GuaTb ∧′= ),()(post , где u′ – новое состоя-
ние агента а, а G – совокупность
mm yxyxyx === :&...&:&: 2211 операторов
присваивания. Здесь mxxx ,...,, 21 – атрибуты
среды или параметры ключевого агента;
myyy ,...,, 21 – выражения соответствующих
типов, также зависящие только от его пара-
метров. Кроме изменения значений пара-
метров, агент может очистить свою вход-
ную очередь, выполняя присваивание
queue(n):=empty. Каждый из операторов
рассматривается как высказывание о том,
что значение атрибута ix после завершения
протокола будет равно значению выраже-
ния iy , вычисленному для значений атрибу-
тов до начала применения протокола.
В случае, когда в предусловии при-
сутствует предикат ), ( zaTIn , предполага-
ется неявное изменение входной очереди
агента. Из нее удаляется первое сообщение.
Кроме того, передачи вызывают изменения
входных очередей соответствующих аген-
тов, путем включения в очередь отправляе-
мых сообщений.
Для функционирования агента необ-
ходимо, чтобы параметры агентов, атри-
буты и состояние агента имели начальные
значения, определяющие начальное состоя-
ние среды. Это состояние однозначно фик-
сирует поведение среды и агентов, погру-
женных в нее. Процесс изменения состоя-
ний среды устанавливается выполнением
базовых протоколов, которые могут функ-
ционировать параллельно и недетерминиро-
вано. Недетерминизм среды определяется
интерливингом при выполнении наблюдае-
мых действий, относящихся к различным
протоколам, а также конкретизацией базо-
вых протоколов, т.е. выбором значений па-
раметров, при которых предусловия стано-
вятся истинными. Конкретная история
функционирования среды описывается од-
ной из возможных последовательностей на-
блюдаемых действий и составляет трассу.
Для общего случая формальное определе-
ние поведения системы, описанной базо-
выми протоколами, было дано в [1].
В дальнейшем рассмотрим системы К-
протоколов, удовлетворяющие требованию
Методи і засоби програмної інженерії
6
однородности, которое означает, что все
базовые протоколы параметризированы
именами своих ключевых агентов. Иными
словами, каждый протокол начинается
квантором общности по имени ключевого
агента. Следует заметить, что требование
однородности не ограничивает общности,
поскольку она сводится к однородному
путем более детальной классификации
агентов по типам.
3. Пример системы заданной базо-
выми К-протоколами
В качестве примера системы, задан-
ной базовыми К-протоколами, рассмотрим
POTS (Plain Old Telephone System), которая
определяет функционирование обычной
телефонной сети. В данной сети функцио-
нируют телефоны – агенты типа Phone и
агент Net типа Network, представляющий
коммутационную систему сети. Агент типа
Phone может находится в следующих со-
стояниях: idle, offhook, dial, dialing, ringing,
busy, fastbusy, ring, offhook_ring, connected.
Агенты имеют имена (номера телефонов), и
базовые протоколы параметризированы
этими именами. Ниже перечислены прото-
колы, ключевой агент которых имеет тип
Phone. Внешний квантор общности, кото-
рый связывает имя ключевого агента n,
присутствует неявным образом.
B1: Phone(n,idle)-> < Out(n,Net,offhook n) >
Phone(n,offhook);
B2: Phone(n,offhook)& In(n,dialtone) -> < >
Phone(n,dial);
B3: Forall m(Phone(n,dial)-> < Out(n,Net,
dial(n,m)) > Phone(n,dialing));
B4: Phone(n,idle)& In(n,ring) -> < >
Phone(n,ring);
B5: Phone(n,dialing)&In(n,ring)-> < >
Phone(n,ringing);
B6: Phone(n,ring)-> <Out(n,Net,offhook n)>
Phone(n, offhook_ring);
B7: Phone(n,connected)-> < Out(n, Net, on-
hook n) > Phone(n, idle);
B8: Phone(n,connected)&In(n, dialtone)-> < >
Phone(n, dial);
B9: Phone(n,dialing)&In(n, busy)-> < >
Phone(n, busy);
B10: Phone(n,ringing)-> <Out(n, Net, onhook
n)> Phone(n, idle);
B11: Phone(n,busy)&In(n, fastbusy)-> < >
Phone(n, fastbusy);
B12: Phone(n,busy)-> <Out(n, Net, onhook
n)> Phone(n, idle);
B13: Phone(n,fastbusy)-> <Out(n, Net, onhook
n)> Phone(n, idle);
B14: Phone(n,dial)&In(n, fastbusy)-> < >
Phone(n, fastbusy);
B15: Phone(n,dial)-> <Out(n, Net, onhook n)>
Phone(n, idle);
B16: Phone(n,offhook_ring)&In(n,
connected)-> < > Phone(n,connected);
B17: Phone(n,ringing)&In(n, connected)-> < >
Phone(n, connected).
Наблюдаемые действия телефонов
состоят в передаче сообщений (сигналов) в
сеть, мгновенно записываемых в очередь
агента Net. Так, например, Out(n,Net,off-
hook n) есть сигнал о снятой трубке,
Out(n,Net,dial(n,m)) – сообщение о том, что
абонент n набрал номер m, Out(n, Net, on-
hook n) – сигнал о том, что трубка абонента
n положена на рычаг. Все сообщения, посы-
лаемые от сети к абоненту, становятся в
очередь и считываются абонентом путем
неявного выполнения внутреннего действия
чтения из своей очереди при проверке пре-
дусловия, содержащего предикат In(n,s). В
частности, принятие сигнала dialtone (про-
верка условия In(n, dialtone)) приводит к по-
явлению непрерывного гудка в трубке; про-
верка In(n,ring) – в телефоне, находящемся в
состоянии idle (трубка лежит на рычаге),
появляется звонок, что выражается в пере-
ходе телефона в состояние Phone(n,ring); тот
же самый сигнал приводит к появлению
длинных прерывистых гудков в снятой
трубке и переводит телефон в состояние
Phone(n, ringing) и т. д. Соответствие тек-
стовых требований и формальных отража-
ется в следующей таблице.
Таблица
B1,
B2
При снятии трубки с неактивного
телефона из сети должен прийти
сигнал длинного непрерывного
гудка
B3 После набора номера сигнал с ад-
ресом вызываемого телефона по-
ступает в сеть
B4, После звонка при поднятии трубки
Методи і засоби програмної інженерії
7
B6,
B16
осуществляется соединение с вы-
зывающим абонентом
B5 После вызова абонента в вызы-
вающий телефон приходит сигнал
вызова
B7 По окончании связи после того,
как трубка положена на рычаг, те-
лефон переходит в неактивное со-
стояние
B8 Если абонент на другом конце
провода положил трубку на рычаг,
приходит сигнал длинного гудка
B9 Если после набора номера, вызы-
ваемый абонент занят, приходит
сигнал «занято».
B10 Если вызывающему абоненту не
удается добиться соединения и он
кладет трубку, телефон переходит
в неактивное состояние
B11 При поднятой трубке после сиг-
нала «занято» может прийти сиг-
нал коротких гудков
B12,
B13
Если трубка поднята и приходит
сигнал «занято», то после того, как
трубка положена на рычаг, теле-
фон переходит в неактивное со-
стояние
B14 При поднятой трубке после длин-
ного гудка в трубке могут поя-
виться короткие гудки
B15 Если трубка поднята и телефон
принимает длинный гудок, трубка
может быть положена и телефон
перейдет в неактивное состояние
B17 После ответа абонента телефоны
соединяются
Как видим, в общем случае нефор-
мальные требования не содержат в явном
виде всех компонентов базового протокола
– предусловие, процесс, постусловие. Кроме
того, ряд существенных условий, которые
входят в предусловие, может быть опущен.
Поэтому одной из задач формализации яв-
ляется явное определение этих компонен-
тов, и восстановление пропущенных усло-
вий.
В рассматриваемом примере пара-
метры агентов и атрибуты среды отсутст-
вуют, поэтому поведение агента определя-
ется только его состояниями. Телефон яв-
ляется недетерминированным агентом, т.е. в
одном и том же состоянии возможно при-
менение различных базовых протоколов.
Например, в состоянии dial можно набрать
номер либо положить трубку.
Агент-коммутатор Net является пол-
ностью детерминированным и его поведе-
ние полностью определяется сообщениями,
которые передаются телефонами. Эти со-
общения, как правило, содержат информа-
цию о новом состоянии телефона, а для
того, чтобы установить следующее дейст-
вие, коммутатор должен знать предыдущее
состояние телефона. Этой цели служит па-
раметр Network Net.phone_state n, где n –
номер телефона. Изменение значений этого
параметра задается присваиваниями в по-
стусловиях базовых протоколов агента Net.
В процессе работы агент типа Network не
меняет своего состояния Active.
C1: Forall n(Network(Net,Active)&
&In(Net,offhook n)&(Network
Net.phone_state n =idle)->
-><Out(Net,n,dialtone)>(Network
Net.phone_state n:=offhook));
C2: Forall(m,n)(Network(Net,Active)&
&In(Net,dial(n,m))&(Network Net.phone_state
m=idle)->
-><Out(Net,n,ring)||Out(Net,m,ring)>((Net-
work Net.phone_state n:=ringing m)&
&(Network Net.phone_state m:=ring)));
C3: Forall(m,n)(Network(Net,Active)&
&In(Net,offhook m)&(Network
Net.phone_state n=ringing m)-><Out(Net,n,
connected)||Out(Net,m, connected)> ((Network
Net.phone_state m:= connected n)&(Network
Net.phone_state n:=connected m)));
C4: Forall(m,n)(Network(Net,Active)&
&In(Net,onhook n)&(Network Net.phone_state
n=connected m)-><Out(Net,m, dial-
tone)>((Network Net.phone_state n:=idle)&
&(Network Net.phone_state m:=offhook)));
C5: Forall(m,n)(Network(Net,Active)&
&In(Net,dial(n,m))&~(NetworkNet.phone_stat
e m=idle)->
-><Out(Net,n,busy)>(Network Net.phone_state
n:=busy));
C6: Forall n(Network(Net,Active)&(Network
Net.phone_state n=busy)->
-><Out(Net,n,fastbusy)>(Network
Net.phone_state n:=fastbusy));
C7: Forall n(Network(Net,Active)&In(Net, on-
Методи і засоби програмної інженерії
8
hook n) -><>(Network Net.phone_state
n:=idle));
C8: Forall n(Network(Net,Active)&(Network
Net.phone_state n=dial)->
-><(Out(Net,n, fastbusy)>(Network
Net.phone_state n:=fastbusy));
C9: Forall n(Network(Net,Active)&In(Net, on-
hook n)&(Network Net.phone_state n=dial)->
-><>(Network Net.phone_state n:=idle));
C10:Forall n(Network(Net,Active)&In(Net,
onhook n)&( Network Net.phone_state
n=busy)->
-><>(Network Net.phone_state n:=idle));
C11:Forall n(Network(Net,Active)&In(Net,
onhook n) &(Network Net.phone_state
n=ringing m)->
-><>(Network Net.phone_state n:=idle)).
4. Непротиворечивость и полнота
базовых К-протоколов
После формализации требований по-
является возможность провести их автома-
тическую верификацию, т.е. проверить вы-
полнение корректности требований по раз-
личным критериям. С другой стороны, по-
скольку формальные требования опреде-
ляют некоторую модель системы, можно
верифицировать различные свойства этой
модели, пользуясь темпоральной логикой и
техникой проверки моделей (model check-
ing). Важными критериями, которые ис-
пользуются при проверке корректности
требований, являются их непротиворечи-
вость и полнота. Содержательная трак-
товка этих понятий зависит от конкретных
приложений и не всегда хорошо формали-
зуется. Однако в ряде случаев можно сфор-
мулировать необходимые или достаточные
критерии для непротиворечивости и пол-
ноты. Проверка этих критериев во многих
случаях позволяет отыскать причины ис-
тинных ошибок в инженерных решениях на
уровне требований.
Рассмотрим критерии, связанные со
следующими требованиями: в любой мо-
мент времени выбор К-протокола для за-
данного ключевого агента должен быть од-
нозначным (непротиворечивость), и если
система не перешла в состояние успешного
завершения своего функционирования, то
должен быть хотя бы один протокол для
продолжения ее функционирования (пол-
нота). Требование непротиворечивости мо-
жет быть ослаблено для тех ситуаций, когда
агенту позволено осуществлять недетерми-
нированный выбор в своих действиях и тем
самым определять свое поведение с помо-
щью различных протоколов.
Достаточными условиями непроти-
воречивости являются невозможность од-
новременного выполнения предусловий
двух различных протоколов, а достаточное
условие полноты выражается как тождест-
венная истинность дизъюнкции всех пре-
дусловий всех протоколов. Формально ус-
ловие непротиворечивости для двух пара-
метризованных базовых протоколов
)( и )( 212121 βαβα >→<∀>→<∀ PyPx
с одним и тем же ключевым агентом, имя
которого входит свободно в протоколы, вы-
ражается в виде отрицания пересечения
формул, выражающих условия примени-
мости протоколов:
))()(( 21 αα yx ∃∧∃¬ .
Два базовых протокола формально
противоречивы, если это условие, называе-
мое условием транзиционной непротиворе-
чивости, не может быть доказано, т.е. явля-
ется выполнимым. При проверке транзици-
онной непротиворечивости необходимо
учитывать следующие обстоятельства. Во-
первых, оно должно выполняться только на
достижимых состояниях системы. Во-вто-
рых, формальная противоречивость может
не быть достаточной для содержательного
противоречия, поскольку недетерминизм,
вызванный этой противоречивостью, может
быть допустимым исходя из инженерных
соображений. Рассмотрим, например, К-
протоколы B7 и B8 формализации требова-
ний к телефонной системе. Формально они
противоречивы, поскольку их условия мо-
гут быть истинными одновременно, и выбор
протокола будет происходить недетермини-
рованным образом. Однако этот недетерми-
низм вполне допустим, поскольку управле-
ние трубкой выполняется пользователем и
она может быть положена до того, как те-
лефон проверит входную очередь сигналов
(сообщений), посланных системой в каче-
стве информации о том, что на другом
конце соединения трубка уже повешена и
телефон должен перейти в состояние dial.
Методи і засоби програмної інженерії
9
Другая ситуация, когда формальная
противоречивость может быть допустимой,
состоит в том, что постусловия протоколов
определяют одинаковые преобразования
состояния среды.
Автоматическая дедуктивная сис-
тема, которая применялась для проверки
требований к телефонной сети, обнаружила
7 противоречивых пар требований. Приме-
ром может служить противоречие между
протоколами B3 и B14. Условие их непро-
тиворечивости
~((Phone(n,dial)& Phone(n,dial)& In(n, fast-
busy)<=> ~((Phone(n,dial)& In(n, fastbusy))
не может быть доказано, и, поскольку в
данном случае недетерминизм недопустим,
обнаруженное противоречие указывает на
возможность ошибки. Такая ошибка на са-
мом деле имеет место, и она должна быть
исправлена путем усиления предусловия К-
протокола B3. Исправленный протокол
имеет вид
B3: Forall m(Phone(n,dial)&emptyq(n)-> <
Out(n,Net,dial(n,m)) > Phone(n,dialing)).
Теперь непротиворечивость становится до-
казуемой, поскольку из In(n, fastbusy) сле-
дует, что очередь сообщений телефона n не
пуста.
Другим примером может служить
обнаруженное противоречие между прото-
колами С7 и С11. Условие их непротиво-
речивости имеет вид:
~(Exist n(Network(Net,Active)&(Network
Net.phone_state n=busy))&
&Exist n(Network(Net,Active)&
&In(Net,onhook
n)&(Network Net.phone_state n=busy))).
Эта формула не может быть дока-
зана, поскольку для некоторого телефона n
может быть истинным условие «трубка на
рычаге» и сигнал об этом стоит первым в
очереди агента Net, а перед этим он воспри-
нимал сигнал «занято». Кроме того, поведе-
ние сети, определяемое этими протоколами,
различно, что нежелательно. Заметим, что
протокол С6 входит в противоречие также и
со всеми другими протоколами, предусло-
вия которых могут быть истинными для те-
лефонов, отличных от n. Следует отметить,
что изменение условия In(Net,onhook n) на
его отрицание не спасает, поскольку новое
требование входит в противоречие с дру-
гими требованиями с позитивным вхожде-
нием условия In для других сообщений.
Аналогичные противоречия возникают
также для протокола C8.
Рассмотренные противоречия легко
разрешаются путем введения нового агента
типа таймера, который будет устанавли-
ваться при переходе некоторого агента в
состояние dial или busy и через некоторое
время сигнализировать сети об истечении
времени, после которого сеть передает те-
лефону установку на короткие гудки.
Протоколы для таймера выглядят
следующим образом:
D1: Timer(T,active)&In(T,start n) -><>
Timer(T,start n);
D2: Timer(T,start n) -><Out(Net,expired n)>
Timer(T,active).
Теперь можно исправить протокол
С6 и добавить управление таймером в C7:
C6.1:Forall n(Network(Net,Active)&In(Net,
expired n)& ~( Network Net.phone_state
n=busy)->
-><Out(Net,n,fastbusy)>(Network(Net, Ac-
tive)&(Network Net.phone_state
n:=fastbusy)));
C6.2:Forall n(Network(Net,Active)&In(Net,
expired n)& ( Network Net.phone_state n=
= dial)-><Out(Net,n,fastbusy)> (Network(Net,
Active)&(Network Net.phone_state
n:=fastbusy)));
C5:Forall(m,n)(Network(Net,Active)&In(Net,d
ial(n,m))& ~(Network Net.phone_state
m=idle)->
->< Out(Net,n,busy) || Out(T,start n)> (Net-
work Net.phone_state n:=busy)).
Аналогичные изменения вводятся в прото-
колы C8 и C1. Противоречие между про-
токолами С4 и С7 устраняется путем уточ-
нения предусловия протокола С7:
C7:Forall n(Network(Net,Active)&
&In(Net,onhook n)&~(Exist m(Network
Net.phone_state n=connected m)-><>
(Network Net.phone_state n:=idle)).
Однородные системы К-протоколов
удобно классифицировать по типам и со-
стояниям ключевых агентов. Достаточным
условием полноты требований является
полнота для всех агентов, находящихся в
одном классе, т.е. имеющих заданный тип и
Методи і засоби програмної інженерії
10
находящихся в заданном состоянии. Кроме
того, удобно ослабить требование полноты,
считая, что для агента с пустой входной
очередью может не быть протокола, опре-
деляющего его функционирование. Таким
образом, условие полноты для класса K(T,s)
базовых протоколов типа T, находящихся в
состоянии s, формулируется следующим
образом:
...))xx(
)n()s,n(T(n
∨∃∨∃→
→¬∧∀
2211 αα
emptyq
,
где ,..., 21 αα - все предусловия базовых
протоколов класса K(T,s), а ,..., 21 xx - спи-
ски их параметров без общего имени ключе-
вого агента n.
Свойства транзиционной непротиво-
речивости и полноты для базовых протоко-
лов рассматриваются для состояний сис-
темы, достижимых из некоторых заранее
заданных начальных состояний системы.
Обычно начальные состояния системы
предполагают пустоту входных очередей,
выделенные начальные состояния агентов,
ограничения на начальные значения пара-
метров. В некоторых случаях могут быть
известны также ограничения на достижи-
мые состояния системы, выраженные в тер-
минах базового языка. Такие ограничения
называются условиями целостности и могут
быть использованы дедуктивной системой в
качестве аксиом для доказательства условий
полноты и непротиворечивости. Условия
целостности обычно формулируются исходя
из содержательных соображений, относя-
щихся к предметной области. Однако они
могут нарушаться в силу противоречивости
требований и должны быть проверены так
же, как и условия транзиционной непроти-
воречивости и полноты.
5. Трассовая генерация и критерии
тестирования
Модель системы, определяемая од-
нородной системой К-протоколов, эквива-
лентна недетерминированной распределен-
ной (параллельной) программе над двух-
уровневой памятью (разделяемая память
среды и локальная память агентов). Если
зафиксировать начальное состояние сис-
темы 0s , которое включает в себя состояние
среды и состояния всех погруженных в нее
агентов, то можем получить все возможные
истории функционирования системы как
последовательности вида
...),(
1
),(
0
222111 → → mnbmnb ss ,
где ),...,(),,( 222111 mnbmnb – конкретизиро-
ванные базовые протоколы, при этом
,..., 21 nn – имена ключевых агентов,
,..., 21 mm – наборы значений остальных
параметров, выполняющих предусловия
базовых протоколов. Поскольку постусло-
вия определяют детерминированные пре-
образования, то состояния ,..., 21 ss одно-
значно определяются начальным состоя-
нием системы и конкретизацией базовых
протоколов. История может быть конечной
или бесконечной. Рассматривая максималь-
ные (не продолжаемые) истории, получим,
что конечные истории оканчиваются либо
успешным завершением (все агенты нахо-
дятся в состоянии Delta), либо тупиковым
состоянием. Заметим, что полнота в классах
базовых протоколов не гарантирует отсут-
ствия тупиковых состояний, поскольку воз-
можно достижимое состояние, при котором
все входные очереди пусты и нет протокола,
функционирующего при пустой входной
очереди (при заданных состояниях агентов).
Если отбросить из истории состояния
системы и оставить только конкретизиро-
ванные протоколы ),...,(),,( 222111 mnbmnb или
процессы (последовательности наблю-
даемых действий), то получим трассу, со-
ответствующую данной истории. Генерация
историй и трасс используется для решения
двух важных задач обработки требований:
проверка достижимости условий и построе-
ние тестов. Тестироваться может как сис-
тема, так и отдельный агент. При тестиро-
вании агента остальные агенты рассматри-
ваются как его окружение. Само тестирова-
ние осуществляется как воздействие
окружения на тестируемый агент. В трассах
входные сообщения, посылаемые из окру-
жения агенту, рассматриваются как управ-
ление, а выходные сообщения агента – как
контролируемая реакция агента.
Генерация трасс может быть органи-
зована как последовательный перебор всех
возможных вариантов применений базовых
протоколов путем движения по дереву по-
ведения системы исходя из некоторых на-
Методи і засоби програмної інженерії
11
чальных состояний. Количество трасс, ко-
торые необходимо сгенерировать для дока-
зательства достижимости условий или по-
крытия фрагментов поведения тестируемого
компонента, даже при конечном множестве
состояний может быть очень большим. По-
этому генерация трасс управляется набором
фильтров, используемых в алгоритме гене-
рации трасс в качестве входной информа-
ции.
К основным фильтрам относятся
следующие:
– условие завершения трассы. Оно
состоит из двух составляющих: утвержде-
ние о состоянии агента и формулы над ат-
рибутами и параметрами агентов. Трасса
прекращает генерироваться, если условие
завершения трассы истинно. Например, при
генерации трасс в вышеуказанной формали-
зации работы телефона условием заверше-
ния трассы может быть утверждение о том,
что данный телефон находится в состоянии
connected. При достижении этого состояния
трасса будет завершена;
– условие исключения состояний.
Фильтр допускает список условий, при вы-
полнении которых прекращается дальней-
шее продвижение по трассе и выполняется
переход к другому варианту;
– другие фильтры определяют такие
параметры генерации, как общее количе-
ство трасс, максимальная длина трассы и
некоторые другие числовые ограничения.
Условия завершения генерации и ус-
ловия исключения состояний могут быть
выражены в терминах линейной темпораль-
ной логики и проверяться синтезирован-
ным по этим условиям автоматом, наблю-
дающим изменение состояний системы в
процессе генерации.
При генерации трасс для тестирова-
ния одного агента удобно пользоваться диа-
граммой переходов этого агента. Эта диа-
грамма есть графическое представление
транзиционной системы, состояниями кото-
рой являются состояния агента, а дейст-
виями – базовые протоколы, конкретизиро-
ванные по имени этого агента. Переходы из
состояния s в состояние s′ размечены базо-
выми протоколами, для которых такой пе-
реход возможен чисто синтаксически, т.е. s
– состояние ключевого агента, а s′ – его но-
вое состояние, которое находится из посту-
словия. На рисунке изображена диаграмма
переходов агента типа Phone.
Рассмотрим все трассы, соответст-
вующие простым путям диаграммы пере-
ходов телефона, начинающиеся и оканчи-
вающиеся в состоянии idle. Их всего 24.
Диаграмма поведения агента отра-
жает возможные трассы без учета состояния
среды и других агентов, погруженных в нее.
Поэтому, вообще говоря, не все трассы дан-
ной диаграммы, возможны. Кроме того,
применение протокола определяет конкрет-
ные значения параметров, от которых он
зависит. Поэтому конкретизированных
трасс может быть больше, чем на диа-
idle
offhook
dial
dialing
ringing
busy
fastbusy
ring
offhook_ring
connected
B1
B2
B3
B4
B5
B6
B7
B9
B8
B10
B11
B12
B13
B14
B15
B16
B17
idle
offhook
dial
dialing
ringing
busy
fastbusy
ring
offhook_ring
connected
B1
B2
B3
B4
B5
B6
B7
B9
B8
B10
B11
B12
B13
B14
B15
B16
B17
Рисунок
Методи і засоби програмної інженерії
12
грамме. В случае рассматриваемого при-
мера только один протокол B3 имеет пара-
метр, отличный от имени ключевого агента.
Конкретизируя этот параметр путем выбора
произвольного имени агента (на самом деле
следует рассмотреть два случая: имя совпа-
дает с именем ключевого агента и отлично
от него), получим уже конкретизированные
протоколы. Поскольку в рассматриваемом
случае все пути возможны, получим, что все
24 трассы могут использоваться для
тестирования телефона. При этом сигналы,
идущие от агента Network, рассматриваются
как управляющие, а сигналы, входящие в
него, как контрольные.
В различных проектах, в которых
приходится тестировать объекты телеком-
муникаций, количество состояний одного
агента сравнительно невелико. Экспонен-
циальный взрыв получается из-за того, что
велико количество агентов и, следова-
тельно, состояний всей системы (не говоря
уже о трассах). Поэтому здесь возникают
следующие вопросы.
• Какое количество трасс необходимо
взять для тестирования продукта?
• Как получить минимальное количе-
ство трасс, достаточное для тестиро-
вания?
Ответы на эти вопросы тесно свя-
заны с критериями, по которым определя-
ются трассы, необходимые для тестирова-
ния. Одним из них будет полное покрытие
требований, выраженных с помощью базо-
вых протоколов. Это означает, что каждый
протокол должен встретиться по крайней
мере один раз хотя бы в одной трассе. Сле-
дует заметить, что трасс с однократным
вхождением базовых протоколов может
быть недостаточно для обнаружения неко-
торых видов ошибок. Например, в протоко-
лах для POTS есть ошибка, состоящая в том,
что входная очередь телефона не очищается
после того, как трубка кладется на рычаг
(что, очевидно, должно делаться путем вы-
полнения присваивания queue(n):=empty в
любом протоколе, в котором телефон пере-
ходит в состояние idle). Эта ошибка может
быть обнаружена только при рассмотрении
трасс, в которых телефон по крайней мере
два раза попадает в состояние idle. Другой
критерий тестирования требует, чтобы лю-
бое возможное сочетание пар базовых про-
токолов входило в некоторую трассу. Такой
критерий позволит обнаружить большее
количество ошибок по сравнению с первым.
К сожалению, проблема построения
полного покрытия требований для произ-
вольных систем однородных К-протоколов
оказывается алгоритмически неразрешимой.
Действительно, для любой машины Тью-
ринга не трудно построить систему из двух
агентов, которая ее моделирует. Поэтому,
чтобы избавиться от трудностей, связанных
с неразрешимостью, необходимо наклады-
вать те или иные ограничения на базовые
протоколы. На самом деле есть достаточно
сильное ограничение, которое выполняется
в большинстве практически важных слу-
чаев. Оно определяется требованием огра-
ниченности времени реакции агентов на
входные воздействия и состоит в следую-
щем. Количество сообщений от одного
агента во входной очереди каждого из них
ограничено некоторой (достаточно малой)
константой. В примере POTS эта константа
равна 1. Действительно, сеть не посылает
агенту сообщений до тех пор, пока не про-
чтет от него очередного сообщения. Той же
самой дисциплины придерживается и каж-
дый агент по отношению к сети.
В следующем разделе рассмотрен ал-
горитм генерации минимального множества
трасс, обеспечивающих полное покрытие
всех базовых протоколов при условии огра-
ниченности очередей и некоторых других
предположениях.
6. Прямая и обратная трассовая гене-
рация и покрытие требований
Построение трасс, покрывающих ба-
зовые протоколы для одного агента, требует
исследования его взаимодействия с окруже-
нием. Для того, чтобы не привязываться к
конкретному окружению, состоящему из
большого количества агентов, а также не
рассматривать все возможные наборы зна-
чений атрибутов, представляющих возмож-
ные начальные состояния среды, можно
воспользоваться абстрактной моделью
среды и символьной трассовой генерацией.
Поведение агента n будем рассматривать
как конечную транзиционную систему с
Методи і засоби програмної інженерії
13
переходами, размеченными базовыми про-
токолами, конкретизированными по ключе-
вому агенту именем n. Состояние среды
будем рассматривать заданным в виде сис-
темы ограничений на значения атрибутов
среды и состояния агентов. Эти ограниче-
ния заданы в виде бескванторной формулы.
В качестве элементарных высказываний
используются равенства и неравенства
термов, а также высказывания вида
), ( zaTIn . Неравенства ... , , ≤< могут
использоваться только для линейных ариф-
метических выражений. Термы строятся из
атрибутов и символов произвольных кон-
стант, используемых для конкретизации ба-
зовых протоколов. Для унификации дейст-
вий, выполняемых в соответствии с базо-
выми протоколами, будем рассматривать
входные очереди как атрибуты среды, па-
раметризованные именами агентов, а их
изменения сделаем явными, добавив в по-
стусловия протоколов, передающих сооб-
щения, соответствующие присваивания.
Поскольку состояния системы опре-
деляются бескванторными формулами, ис-
числение предикатов неоднозначно, пере-
ходы абстрактной модели системы, исполь-
зуемые для порождения трасс, определя-
ются с помощью предикатных трансформе-
ров [1], т.е. формульных преобразований.
Их можно определить следующим образом.
Пусть )),(),((:)( xrPxrxnb βα >→<∀ есть
базовый протокол, конкретизированный
именем ключевого агента n. Квантор
общности связывает переменные типа «имя
агента», символьного или арифметического
типа. Конкретизируем протокол, выбирая в
качестве значений переменных символы
произвольных констант соответствующего
типа. В качестве значений имен агентов
можно использовать имена, уже присутст-
вующие в состоянии среды, или ввести но-
вое имя в виде произвольной константы
типа «имя агента». Конкретизированный
протокол
)),(),((:),( mrPmrmnb βα >→<
получается подстановкой параметров в
формулы пред- и постусловий. Для К-про-
токолов постусловие состоит из присваи-
ваний и предположения T(n,s) о новом со-
стоянии агента. Можно предположить, что
состояния агента n не зависят от парамет-
ров. Это не ограничивает общности, по-
скольку запоминание параметров можно
обеспечить путем установки соответствую-
щего атрибута агента. Изменение состояния
среды определяется с помощью предикат-
ного трансформера следующим образом.
Разделим множество атрибутов
,...),( 21 rrr = , использованных в протоколе,
на те, которые встречаются в левых частях
присваиваний, и все остальные. Обозначим
список первых ,...),( 21 uuu = и остальных
,...),( 21 vvv = . Изменение состояния среды
),( vuγ определяется с помощью прямого
предикатного трансформера, который
имеет следующий вид:
),(),...)),(
),,((),...,,(,...)(,(
...))),(:),(:(),,((
2
2112121
2211
vuvcf
uvcfuvcccc
vufuvufuvu
γ
γ
γ
′==
==∧∃=
=∧=∧=pt
При вычислении предикатного трансфор-
мера формула ),( vuγ ′ подвергается некото-
рым упрощениям, зависящим от предмет-
ной области. В частности, могут приме-
няться известные процедуры элиминации
кванторов для линейной арифметики и аб-
страктных типов данных, используемых при
формализации требований. Если состояние
среды конкретно, т.е. все атрибуты имеют
конкретные значения, ),( vuγ ′ получается
простой подстановкой этих значений. Дей-
ствительно, в этом случае
...)
...(),(
221
12211
∧=∧=
=∧∧=∧==
eve
vduduvuγ
и, следовательно,
...)...),(
),((),(
22112
211
∧=∧=∧∧=
=∧==′
evevvdf
uvdfuvuγ
.
Отметим важное свойство предикатного
трансформера – его монотонность. Оно оз-
начает следующее: если 21 γγ → , то
),(),( 21 βγβγ ptpt → .
Определим теперь отношение пере-
ходов среды:
,
),(),(
),(),()),,((),(
),( vuvu
vuvumnbvu
mnb γγ
γγγ
′′ →
′→′′→ pre
где ))),((),,((),( mnbvuvu postpt γγ =′ . При-
меняется это правило следующим образом.
Пусть среда находится в состоянии ),( vuγ .
Выберем базовый протокол b(n) и его кон-
Методи і засоби програмної інженерії
14
кретизацию b(n,m) таким образом, что пре-
дусловие конкретизированного протокола
выполняется на состоянии ),( vuγ
( )),((),( mnbvu pre→γ ). Вычислим значение
предикатного трансформера ),( vuγ ′ на со-
стоянии среды и постусловии конкретизи-
рованного протокола, затем возьмем неко-
торую формулу ),( vuγ ′′ , из которой следует
полученное значение. В результате полу-
чим, что среда может переходить с помо-
щью протокола b(n,m) из состояния ),( vuγ
в новое состояние ),( vuγ ′′ . Таким образом,
при переходе среды в новое состояние оно
может усиливаться. Различные стратегии
ослабления зависят от приложений, но здесь
можно отметить некоторые из них. Если γ ′
имеет вид дизъюнкции, то можно оставить
только один из дизъюнктивных членов, что
даст возможность применить базовый про-
токол, предусловие которого может быть
сопоставлено с этим членом. Заметим, что
каждое условие покрывает некоторое мно-
жество состояний (именно тех, на которых
условие истинно), а применимость базового
протокола означает его применимость на
всех состояниях покрываемого множества.
Усиление условия сокращает множество
состояний, которые им покрываются и, сле-
довательно, расширяет возможности при-
менения базовых протоколов.
Определим теперь среду для генера-
ции трасс. Она рассматривается как среда
][sγ с погруженным в нее одним ключевым
агентом. Отношение переходов в этой среде
определяется следующими правилами:
][][
,
),(
),(),(
ss
ss
mnb
mnbmnb
′′ →
′ →′ →
γγ
γγ
,
(переход агента)
][][
),(
ss
mnb
γγ
γγ
′→
′ → ′
, (переход среды)
где n′ – имя агента, отличное от n. Генера-
ция трасс управляется критерием покрытия
(однократное покрытие всех протоколов,
покрытие всех парных сочетаний и т.д.), ус-
ловием завершения и подходящими фильт-
рами. В условии завершения можно исполь-
зовать критерий покрытия (процесс генера-
ции завершается, если покрытие уже обес-
печено). Для этой цели в состояние среды
следует ввести дополнительный компонент,
в котором накапливается информация о
степени покрытия (например, множество
уже пройденных протоколов, которое по-
полняется при каждом переходе). Фильтруя
трассы по максимальной допустимой длине,
можно получить процесс, при котором ге-
нерация происходит по дереву поведения
агента, обходя его в глубину или в ширину.
При этом в точках возврата при недетерми-
нированном выборе следующего шага
можно отдавать предпочтение еще не прой-
денным протоколам.
В общем случае сложность процесса
генерации определяется недетерминизмом
при выборе подходящей конкретизации
протоколов и работой алгоритмов дедук-
тивной системы (прувер и солвер). Значи-
тельное повышение эффективности можно
получить, если накладывать те или иные
ограничения на базовые протоколы.
Рассмотрим, например, следующие
ограничения.
• Области значений символьных атри-
бутов представляют собой конечные
области без операций и предикатов
(перечислимые типы).
• Параметризация протоколов (внеш-
ний универсальный квантор) осуще-
ствляется только по символьным пе-
ременным и именам агентов.
• Каждый протокол изменяет входную
очередь одного агента и читает из
своей очереди не более чем по од-
ному разу.
• Глобальные атрибуты отсутствуют.
• Длина любой входной очереди не
превосходит 1.
При этих ограничениях алгоритм генерации
трасс может быть описан следующим обра-
зом.
Прямая генерация трасс.
Вход: начальное состояние 0s клю-
чевого агента n, ограничения (формула 0γ ),
определяющие начальное состояние среды
(в случае отсутствия ограничений формула
равна 1), критерий покрытия, условие за-
вершения трассы и другие фильтры.
Выход: множество сгенерированных
трасс, обеспечивающих максимальное по-
крытие требований по заданному критерию.
Методи і засоби програмної інженерії
15
В процессе генерации строятся те-
кущая история
][...][][ 21
1100 kk
bbb sss k γγγ →→→
и текущее состояние системы ][ kk sγ . В те-
кущей истории выделены состояния, отлич-
ные от текущего и называемые точками
возврата. Для каждой из точек возврата
задано множество всех переходов из этой
точки из всех возможных, которые еще не
пройдены. Кроме того, в каждый момент
генерации задано множество уже построен-
ных трасс и объект cover, определяющий
текущее покрытие требований (например,
множество уже пройденных базовых прото-
колов для критерия однократного прохож-
дения). Процесс генерации завершается,
если выработано условие окончания гене-
рации или осуществлено покрытие (объект
cover находится в состоянии завершения).
1. В качестве начальной текущей исто-
рии выбираем историю, состоящую
из одного текущего состояния
][ 00 sγ . Множество пройденных
трасс пусто, объект cover находится
в начальном состоянии (нулевое по-
крытие), генерация не закончена. Да-
лее выполняется цикл, включающий
следующие пункты.
2. Если состояние объекта cover гово-
рит о том, что покрытие осуществ-
лено, то процесс генерации останав-
ливается, возвращает построенные
трассы и сообщает о полном покры-
тии.
3. Если выполняется условие заверше-
ния трассы, то трасса добавляется к
множеству уже построенных трасс.
Если в текущей истории есть точки
возврата, то происходит «откат» к
ближайшей из них, иначе вырабаты-
вается условие завершения генера-
ции. Цикл повторяется.
4. Если один из фильтров запрещает те-
кущее состояние и есть точки воз-
врата, то происходит «откат» к бли-
жайшей из них, иначе вырабатыва-
ется условие завершения генерации.
Цикл повторяется.
5. Если текущее состояние есть точка
возврата, то выбирается следующий
переход, история продолжается на
один шаг, цикл повторяется. При
этом если переход был последним, то
признак точки возврата снимается.
6. Находим все переходы агента n из
текущего состояния, выбирая приме-
нимые базовые протоколы и их до-
пустимые конкретизации. Если при
своем переходе агент посылает со-
общение, то к состоянию среды до-
бавляем соответствующие ограниче-
ния на очереди других агентов.
7. Если входная очередь ключевого
агента пуста, то рассматриваем все
допустимые переходы среды, кото-
рые изменяют входную очередь
ключевого агента. Для этого, воз-
можно, потребуется добавить допол-
нительные ограничения к состоянию
среды. Для любого такого перехода
добавляем все допустимые переходы
ключевого агента и новые переходы
к множеству уже построенных.
8. Если количество построенных пере-
ходов больше 1, объявляем текущее
состояние точкой возврата.
9. Если в результате выполнения пп. 6
и 7 не найдено ни одного перехода,
выполняем откат к точке возврата
или вырабатываем признак оконча-
ния генерации, если точек возврата
больше нет.
10. Если переходы есть, то выбираем
один из переходов в текущем со-
стоянии и продолжаем текущую ис-
торию на один шаг. Повторяем цикл.
В рассмотренном алгоритме допол-
нительных пояснений требуют п. 6 и 7.
Первый соответствует правилу перехода
агента, второй – правилу перехода среды.
Переход агента (вместе со средой, к
которой относим заполнение его входной
очереди) выполняется с помощью преди-
катного трансформера. Рассматриваем со-
стояние среды γ и протокол b, параметри-
зованный именем ключевого агента. Пред-
полагаем, что состояние среды имеет вид
конъюнкции. Если протокол параметризи-
рован, то сначала находим значения пара-
метров ,...),( 21 mmm = такие, что формула
),,(),( mvuvu αγ → истинна. Для символь-
ных параметров решения находятся пере-
Методи і засоби програмної інженерії
16
бором, а для имен агентов выбираем реше-
ния из набора имен, которые участвуют в
состоянии среды плюс одно новое имя. Для
уменьшения перебора можно рассматривать
символьные переменные типа неизвестные
и откладывать присваивание им значений
до тех пор, пока возможно.
После построения формулы ),( vuγ ′
элиминируем кванторы существования и
упрощаем полученную формулу. Затем
приводим ее к дизъюнктивной нормальной
форме и каждый из конъюнктов выбираем в
качестве нового состояния среды.
Переходы среды выполняются так
же, как и переходы агента, но выбираются
только такие, которые изменяют состояние
входной очереди ключевого агента. Если
таковых нет, то следует рассмотреть пере-
ходы среды некоторой ограниченной
длины, приводящие в конце концов к из-
менению входной очереди ключевого
агента.
Обратная генерация трасс.
Другой подход к генерации трасс со-
стоит в обратном прохождении трассы с
помощью обратного предикатного транс-
формера, который определяется следую-
щим образом:
)),...,,(),,((...))),(:
:),(:(),,...,,((
212
21121
1
vvufvufvuf
uvufuvuu
γ
γ
=∧=
=∧=−pt
(при тех же обозначениях, что и в опреде-
лении pt). Связь между двумя трансформе-
рами выражается следующим образом:
.)),,((
);),,((
1
1
γββγ
ββγγ
⇒
⇒
−
−
ptpt
ptpt
Действительно, пользуясь очевидными со-
кращениями, получаем
...);),(
),(),(),(),((
)...),),(),(
),((()),),,(((
2
211
221
1
11
∧=
=∧=∧∃⇔
⇔∧=∧=
=∧∃⇔ −−
vcf
vufvcfvufvcc
vcfuvcf
uvccvu
γ
β
γββγ ptptpt
);),),,(((
...)),(),(),(
),(),((...)),(
),(),(),((),(),(
1
221
12
211
ββγ
γ
γγ
vu
vcfvufvcf
vufvccvuf
vufvufvufvuvu
ptpt −⇔
⇔∧=∧=
=∧∃⇒∧=
=∧=∧⇔
).,(...)),(),(
(),(...)),(
),(),((...)),(
),()),...,,(
),,((()),),...,,(
),,((()),),,(((
221
122
112
2112
12
1
1
vuvcfuvcf
ucvuvcfu
vcfuvucvcf
uvcfuvvcf
vcfcvvuf
vufvu
γ
γ
γ
γβ
γββγ
⇒∧=∧=
=∃∧⇔∧=∧
∧=∧∃⇔∧=
=∧=∧
∃⇔
⇔− ptptpt
Обратную генерацию трасс можно
получить в системе, определяемой следую-
щими правилами:
][][
,
),(
),(),(
1
ss
ss
mnb
mnbmnb
γγ
γγ
→′′
′ →′ →
− ,
][][
),(
ss
mnb
γγ
γγ
→′
′ → ′
.
В этой среде все стрелки перевернуты в об-
ратном направлении, а переходы размечены
теми же самыми переходами, но с отрица-
тельным показателем, указывающим на то,
что речь идет об обратных преобразованиях
(от постусловий к предусловиям). При этом
)),((),(
)),((),(
1
1
mnb
mnb
′∧′=
∧′=
−
−
prept
или prept
βγγ
βγγ
соответственно. Условием завершения об-
ратной генерации является переход в на-
чальное состояние, начинать следует от со-
стояний, в которые ведут еще не пройден-
ные переходы.
Преимущества обратной генерации
состоят в следующем:
• Обратный предикатный трансфор-
мер обычно вычисляется легче, чем
прямой (подстановка вместо реше-
ния уравнений и неравенств)
• Достигнув начального состояния,
получаем значения атрибутов, с ко-
торых следует начинать тестирова-
ние по данной трассе.
Другим применением обратной гене-
рации является возможность определения
начальных значений для трасс, полученных
с помощью прямой генерации.
7. Факторизация пространства со-
стояний агента
Критерия покрытия всех требований
может быть недостаточно, чтобы создать
исчерпывающий тестовый набор, так как он
не будет содержать всех поведений и изме-
Методи і засоби програмної інженерії
17
нений атрибутов и параметров. Использо-
вание более точных критериев покрытия
приводит к «экспоненциальному взрыву»
количества трасс, необходимых для выпол-
нения такого критерия. Существенное
уменьшение количества трасс можно полу-
чить путем факторизации пространства
состояний агента (разбиения этого про-
странства на классы), построения полного
набора трасс внутри каждого из классов, а
затем связывания классов с начальными и
заключительными состояниями системы
небольшим количеством трасс.
Разбиение пространства состояний
агента на классы может происходить раз-
личными способами. Один из практических
подходов состоит в том, чтобы строить раз-
биение в соответствии с классификацией
требований по функциональностям. Это
разбиение фактически может быть опреде-
лено структурой разделов исходной доку-
ментации, которая используется при форма-
лизации требований. Другой подход заклю-
чается в том, чтобы осуществлять разбиение
пространства состояний по количеству свя-
зей, концентрируя в разных классах состоя-
ния с большим количеством связей и
уменьшая их между классами.
Факторизация пространства состоя-
ний агента индуцирует факторизацию со-
стояний всей системы на классы, каждый из
которых состоит из достижимых состояний,
для которых состояние заданного (ключе-
вого) агента находится в одном и том же
классе состояний этого агента.
Снова для генерации трасс будем
проводить символьное моделирование, рас-
сматривая состояния системы заданными в
виде ][sγ , где γ – формула, ограничиваю-
щая атрибуты, а s – состояние агента. Абст-
рактные состояния такого типа разбиваются
на классы по принадлежности определен-
ному классу состояния ключевого агента. В
каждом классе абстрактных состояний вы-
делим в качестве начальных те, в которые
можно попасть из других классов, а в каче-
стве заключительных такие, из которых
возможны переходы в другие классы. Более
точно, пусть ss nb ′→ )( , где s и s′ – состоя-
ния агентов, которые принадлежат разным
классам, )),(),((:)( mrPmrmnb βα >→<∀ –
базовый протокол, параметризованный
именем ключевого агента. ])[,( smrm α∃ бу-
дем рассматривать как заключительное
состояние класса, которому принадлежит s,
а ]))[,(),,(( smrmrm ′∃ βαpt – как начальное
состояние класса, которому принадлежит s′ .
Для того чтобы уменьшить количество на-
чальных и заключительных состояний в
классе, воспользуемся следующим прие-
мом. Пусть ],...[],[ 21 ss γγ – все начальные
(заключительные) состояния с одним и тем
же состоянием s ключевого агента. Заменим
их одним ]...)[( 21 s∨∨ γγ . Теперь для каж-
дого состояния ключевого агента будет
только одно начальное состояние системы в
классе.
Перейдем к построению тестовых
трасс. Выберем начальное состояние сис-
темы ][ 00 sγ . Класс 0K , содержащий его,
объявим начальным классом и добавим это
состояние к начальным состояниям класса,
определенным выше. В качестве критерия
покрытия требований выберем критерий
однократного прохождения всех базовых
протоколов (независимо от конкретизации).
В каждом классе с помощью обратного
символьного моделирования построим
множество трасс соединяющих начальные и
заключительные состояния класса, так,
чтобы обеспечить покрытие всех требова-
ний внутри класса. Естественно, что все
трассы построить невозможно, поскольку
могут быть циклы. Поэтому накладываем
некоторые ограничения с помощью фильт-
ров, а также на повторяемость цикла. За-
ключительные состояния, из которых на-
чальные оказались недостижимыми, отбра-
сываем вместе со всеми переходами, веду-
щими в них, отмечая наличие таких состоя-
ний как предупреждение о возможной
ошибке.
Для каждой трассы внутри класса
обратное моделирование дает возможность
усилить начальное состояние этой трассы и,
проходя повторно ту же самую трассу в
прямом направлении, усилить также и за-
ключительное состояние этой трассы с по-
мощью предикатных трансформеров. Пусть
][...][][ 21
1100 kk
bbb sss k γγγ →→→ – ис-
тория обратного прохождения трассы
),...,,( 21 kbbb из заключительного состояния
Методи і засоби програмної інженерії
18
][ kk sγ в начальное ][ 00 sγ . Переход из
][ 11 ++ ii sγ в ][ ii sγ выполняется с помощью
обратного трансформера, а применение
прямого трансформера усиливает усло-
вие 1+iγ .
Определим на множестве классов от-
ношение переходов, полагая, что
KK nb ′→ )( , если для некоторого заключи-
тельного состояния Ks ∈ класса K сущест-
вует начальное состояние Ks ′∈′ такое, что
ss nb ′→ )( . Если в этой системе есть
классы, не достижимые из 0K , то отбросим
их вместе с переходами, сгенерировав со-
общение о возможной ошибке. Поскольку
классы определяются состояниями ключе-
вых агентов, то протоколы, соединяющие
разные классы, не входят в множество про-
токолов, действующих внутри классов. По-
этому для каждого класса K продолжим все
трассы, построенные для него, на один шаг,
добавляя соответствующие протоколы, ве-
дущие в соседний класс. Теперь для каж-
дого класса K задано множество трасс, со-
единяющих начальные состояния этого
класса с начальными состояниями всех
смежных, и для каждого начального состоя-
ния ][sγ любого из классов K, достижимых
из 0K , можно построить историю, соединя-
ющую начальное состояние системы с
состоянием ][sγ . Действительно, по
определению, для состояния ][sγ найдется
заключительное состояние ][s′′γ в некото-
ром смежном классе nK такое, что
][][ ss b γγ →′′ . Поскольку nK достижим из
начального состояния, можно построить ис-
торию, соединяющую 0K с K:
KKKK b
n
bbb k →→→→ ...21
10 .
Далее, выбирая подходящие истории внутри
классов, получим историю, соединяющую
][ 00 sγ и ][sγ . Теперь для каждого класса
возьмем все построенные для него трассы,
соединим их с начальным состоянием и
получим набор трасс, обеспечивающих
однократное покрытие. Количество трасс в
наборе не будет превосходить суммы коли-
чества трасс в каждом классе.
Заключение
Описанная технология была успешно
применена в проекте VRS на примерах ин-
дустриальных проектов. Входом для пер-
вого этапа технологической цепочки явля-
лась документация, в которой требования
были выражены на естественном языке.
Необходимо было формализовать их и
представить в виде базовых протоколов
посредством MSC-диаграмм.
Создание базовых протоколов осу-
ществлялось через специальную оболочку
для их ввода. Сначала определялись агенты
и их параметры в виде описания среды.
Синтаксис грамматики представления аген-
тов проверялся специальным валидатором,
что уменьшало появление ошибок на этапе
верификации требований. Базовые прото-
колы вводились в графическом виде. После
того как данные были подготовлены, на
втором этапе проводилась проверка транзи-
ционной непротиворечивости, полноты и
достижимости требований. При проверке
выдавались трассы с указанием ошибок и
неточностей в требованиях. После отладки
требований на третьем этапе выполнялась
генерация трасс, предназначенных для тес-
тирования. Полученные трассы использова-
лись в тестировании уже готовой системы,
созданной на основе требований.
Благодарности Ю.В. Капитоновой,
А.А. Летичевскому, В.П. Котлярову и А.Б.
Годлевскому за ценные советы и помощь в
подготовке материала.
1. International Telecommunications Union. Recom-
mendation Z. 120–Message Sequence Chart (MSC).
–1999.
2. International Telecommunications Union. Recom-
mendation Z. 100–Specification and Description
Language (SDL). –1999.
3. Object Management Group. Unified Modeling Lan-
guage Specification, 2.0. –2003.
4. Спецификация систем с помощью базовых
протоколов / А.А. Летичевский, Ю.В. Капитоно-
ва, А.А. Летичевский (мл.) и др. // Кибернетика и
системный анализ. – 2005. – №4. – С.3–21.
5. Basic Protocols, Message Sequence Charts, and
theVerification of Requirements Specifications /
A.A. Letichevsky, J.K. Kapitonova, A.A. Letichev-
sky Jr. et all.// Proc. Intern. Workshop, WITUL’04,
Rennes (France). – 2004. – P.30–38.
6. Leveraging UML to deliver correct telecom
applications in UML for Real: Design of Embedded
Real-Time Systems / S. Baranov, C. Jervis, V. Kot-
Методи і засоби програмної інженерії
19
lyarov, A. Letichevsky, T. Weigert // L.Lavagno, G.
Martin, and B. Selic, Kluwer Academic Publ. –
2003. – Р.323–342.
7. Инсерционное программирование / А.А. Летичев-
ский, Ю.В. Капитонова, А.А. Летичевский (мл.)
и др. // Кибернетика и системный анализ. –
2003. – №1. – С.19–32.
Получено 02.06.05
Об авторе
Летичевский Александр Александрович
ведущий программист
Место работы автора:
ООО «Информационные Программные
Системы»
03680, Киев, ул. Боженко, 15
Тел. 490 5424 (раб.), 257 6788 (дом.)
E-mail: lit@iss.org.ua
|
| id | nasplib_isofts_kiev_ua-123456789-1318 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 1727-4907 |
| language | Russian |
| last_indexed | 2025-12-01T19:47:37Z |
| publishDate | 2005 |
| publisher | Інститут програмних систем НАН України |
| record_format | dspace |
| spelling | Летичевский, А.А. 2008-07-25T15:36:39Z 2008-07-25T15:36:39Z 2005 Об одном классе базовых протоколов / А.А.Летичевский // Проблеми програмування. — 2005. — N 4. — С. 3-19. — Бібліогр.: 7 назв. — рос. 1727-4907 https://nasplib.isofts.kiev.ua/handle/123456789/1318 623 518.3 517.5 Рассматривается проблема представления требований к поведению интерактивной системы в виде формальных спецификаций, а также ее верификация и генерация трасс, используемых для создания тестовых наборов. Исследуется специальный класс спецификаций, представленный в виде базовых протоколов, в котором рассматриваются возможные виды противоречивости и неполноты. С помощью символьного моделирования требований, производится порождение символьных трасс, используемых для тестирования создаваемой системы по различными критериями. ru Інститут програмних систем НАН України Методи і засоби програмної інженерії Об одном классе базовых протоколов On the One Class of Basic Protocols Article published earlier |
| spellingShingle | Об одном классе базовых протоколов Летичевский, А.А. Методи і засоби програмної інженерії |
| title | Об одном классе базовых протоколов |
| title_alt | On the One Class of Basic Protocols |
| title_full | Об одном классе базовых протоколов |
| title_fullStr | Об одном классе базовых протоколов |
| title_full_unstemmed | Об одном классе базовых протоколов |
| title_short | Об одном классе базовых протоколов |
| title_sort | об одном классе базовых протоколов |
| topic | Методи і засоби програмної інженерії |
| topic_facet | Методи і засоби програмної інженерії |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/1318 |
| work_keys_str_mv | AT letičevskiiaa obodnomklassebazovyhprotokolov AT letičevskiiaa ontheoneclassofbasicprotocols |