ПРОГРАММИРОВАНИЕ, 2013, No 6, с. 12-24
ТЕСТИРОВАНИЕ, ВЕРИФИКАЦИЯ И ВАЛИДАЦИЯ ПРОГРАММ -
УДК 681.3.06
СОГЛАСОВАНИЕ КОНФОРМНОСТИ И КОМПОЗИЦИИ
© 2013 г. И.Б. Бурдонов, A.C. Косачев
Институт системного программирования РАН 109004 Москва, ул. А. Солженицына, 25 E-mail: igor@ispras.ru, kos@ispras.ru Поступила в редакцию 12.06.2013
*
В нашей предыдущей статье [1] предлагалась новая модель реализации типа ЬТБ. В обычной ЬТБ переходы помечаются действиями, поэтому её можно назвать ЬТБ действий. Новая модель - ЬТБ наблюдений, в ней вместо действий используются наблюдения и тестовые воздействия (кнопки). Эта модель обобщает многие семантики тестирования, которые опираются на ЬТБ действий, но используют дополнительные наблюдения (отказы, множества готовности и т.п.). Кроме того, единообразно моделируются системы с приоритетами, которые не описываются с помощью ЬТБ действий. В данной статье мы развиваем этот подход, концентрируя внимание на композиции систем. Дело в том, что на трассах наблюдений невозможно определить такую композицию, по отношению к которой композиция 1ЛБ обладала бы свойством аддитивности: множество трасс композиции ЬТБ совпадает с множеством всех попарных композиций трасс ЬТБ-операндов. Это объясняется тем, что наблюдение в композиционном состоянии не вычисляется по наблюдениям в состояниях-операндах. В данной статье мы предлагаем подход, устраняющий этот недостаток. Для этого переходы ЬТБ помечаются такими символами (событиями), которые, с одной стороны, можно компоновать для обеспечения свойства аддитивности, а, с другой стороны, можно использовать для генерации наблюдений при тестировании: переход по событию приводит к возникновению связанного с этим событием наблюдения. Эта модель названа ЬТБ событий. В статье определяется 1) преобразование ЬТБ событий в ЬТБ наблюдений для согласования с положениями нашей предыдущей статьи [1], 2) композиция ЬТБ событий, 3) композиция спецификаций, сохраняющая конформность: композиция конформных реализаций конформна композиции спецификаций, 4) единообразное моделирование ЬТБ действий через ЬТБ событий, которое позволяет рассматривать реализацию в любой семантике взаимодействия, допустимой для ЬТБ действий. При этом композиция ЬТБ событий, полученных в результате моделирования исходных ЬТБ действий, эквивалентна ЬТБ событий, полученной в результате моделирования композиции этих ЬТБ действий.
1. ВВЕДЕНИЕ
Основной моделью взаимодействующих процессов является LTS (Labelled Transition System). Для неё были определены операции алгебры процессов и, прежде всего, операция параллельной композиции LTS. Тестирование понимается как взаимодействие реализации с тестовой системой, формализуемое как параллельная композиция LTS-реализации с LTS-тестом. При этом первоначально предполагалось, что единственными
* Работа выполнена при частичной поддержке гранта РФФИ №13-07-00915.
наблюдениями над LTS являются внешние (наблюдаемые) действия, которыми помечены переходы LTS. Допускается также ненаблюдаемая внутренняя активность, которая в LTS изображается переходами по внутренним (ненаблюдаемым) действиям, которые только меняют состояние LTS. Поскольку такие действия не наблюдаемы, они не различимы при тестировании и обозначаются одним символом т. Такую модель можно назвать LTS действий или ATS1. Результатом тестирования является последова-
1аА" - от англ. "action" - действие.
тельность наблюдаемых действий - трасса действий. На трассах действий можно так определить композицию трасс, что тестирование и композиция LTS оказываются согласованными: множество трасс композиции LTS совпадает с множеством всех попарных композиций трасс LTS-операндов. Это свойство можно назвать аддитивностью трасс относительно композиции.
Другая (но тесно связанная с алгеброй процессов) формализация тестирования опирается на так называемую машину тестирования [7, 8, 9], которая фиксирует те или иные возможности тестовой системы по управлению и наблюдению за поведением реализации. Предполагается, что с помощью машины тестирования можно разрешать или запрещать реализации выполнение переходов по тем или иным внешним действиям. При этом т-активность всегда разрешена. Сразу же выяснилось, что, кроме действий, при тестировании возможны и другие наблюдения. Так или иначе, все они связаны с наблюдением остановки LTS-реализации, которая возникает, когда текущее состояние стабильно (в нём нет тт
но выполнение определённых в состоянии переходов по внешним действиям, поскольку все они в данный момент времени запрещены машиной тестирования. Такими наблюдениями, кроме самого факта остановки, являются, в частности, отказ (refusal set) и множество готовности (ready set). Отказ - это множество действий, которые машина тестирования разрешает выполнять, но в текущем состоянии реализации нет переходов по этим действиям. Если мы наблюдаем остановку машины при том или ином множестве разрешённых внешних действий, то тем самым мы наблюдаем соответствующий отказ. Множество готовности - это множество всех внешних действий, по которым есть переходы в текущем состоянии реализации. Такое наблюдение характерно, например, для систем с графическим интерфейсом, когда на экран выдаётся "меню" возможных действий, и система ждёт от пользователя выбора того или иного действия. Теперь результатом тестирования оказывается трасса наблюдений, в которую могут входить не только внешние действия, но и другие наблюдения. Набор допустимых тестовых воздействий и наблюдений формализу-
ет возможности тестовой системы и задаётся семантикой взаимодействия. Например, хорошо известное отношение конформности toco (Input Output Conformance) [11, 12], опирающееся на разделение действий на стимулы (input) и реакции (output), допускает два вида тестовых воздействий - посылку одного стимула или приём всех реакций, и единственный вид отказа - отсутствие реакций (quiescence).
Недостатком такой формализации является то, что все наблюдения, кроме внешних действий, описываются LTS-моделью неявно. Кроме того, тестовое воздействие, по сути, сводится к множеству разрешаемых им внешних действий. Всё это, во-первых, усложняет интерпретацию модели при тестировании, во-вторых, не даёт свободы в рассмотрении новых видов наблюдений и тестовых воздействий для той или иной семантики взаимодействия и, в-третьих, не даёт возможности в самой модели реализации явно определять те тестовые воздействия, на которые она реагирует теми или иными явно задаваемыми наблюдениями.
В нашей предыдущей статье [1] мы попытались избавиться от этого недостатка, определив новую обобщённую модель LTS. В этой модели переходы помечены не внешними действиями, а наблюдениями или тестовыми воздействиями, которые названы кнопками. Кроме свободы в соотношении кнопок и наблюдений в реализации, это дало возможность единообразно моделировать также системы с приоритетами, которые не описываются с помощью LTS действий. Эту новую модель можно назвать LTS наблюдений или OTS2.
Однако остался ещё один существенный общий недостаток как LTS наблюдений, так и LTS действий при рассмотрении трасс не только действий, но и других наблюдений. Дело в том, что переход от действий к наблюдениям приводит к рассогласованию тестирования с композицией LTS: на трассах наблюдений невозможно определить композицию так, чтобы выполнялось свойство аддитивности. Это объясняется тем, что, вообще говоря, наблюдение в композиционном состоянии не вычисляется по наблюдениям в состояниях-операндах. Единственным ис-
2"0" - от англ. "observation" - наблюдение.
ключением, кроме внешнего действия, является множество готовности.
В данной статье мы предлагаем подход, устраняющий этот недостаток. Идея заключается в том, чтобы помечать переходы LTS такими символами (мы их назвали событиями), которые, с одной стороны, можно компоновать для обеспечения свойства аддитивности, а, с другой стороны, можно использовать для генерации наблюдений при тестировании: переход по событию приводит к возникновению того или иного связанного с этим событием наблюдения. Последнее свойство можно назвать генеративностыо трасс событий: по ним вычисляются все трассы наблюдений реализации. Такую модель можно назвать LTS событий или ETS3.
Мы определим 1) преобразование ETS в OTS для согласования с положениями нашей предыдущей статьи [1], 2) композицию ETS, 3) композицию спецификаций, сохраняющую конформность: композиция конформных реализаций конформна композиции спецификаций, 4) единообразное моделирование ATS через ETS, которое позволяет рассматривать реализацию в любой семантике взаимодействия, допустимой для ATS. Здесь мы ставим себе целью обеспечить следующее важное свойство согласованности композиции и моделирования: композиция ETS-операндов, полученных в результате моделирования исходных ATS-операндов, эквивалентна ETS, полученной в результате моделирования композиции этих ATS-операндов. Здесь эквивалентность понимается как равенство множества трасс событий.
2. LTS СОБЫТИЙ И ГЕНЕРАЦИЯ НАБЛЮДЕНИЙ ПО СОБЫТИЯМ
Под LTS (Labelled Transition System) понимается ориентированный граф с непустым множеством вершин, которые называются состояниями, одно из состояний выделено как начальное, дуги называются переходами и помечены символами из некоторого универсума символов L или специальным символом внутреннего действия т £ L. Мы также вводим специальный дополнительный символ разрушения 7 £ L, моделирующий любое поведение LTS, которое нежелательно при взаимодействии с ней [2,3,6]. LTS S
3"Е" - от англ. "event" - событие.
задаётся четвёркой S = Lts(Vs,Es,so), где Vs -множество состояний, Es С Vs х (Z U {т}) х VS -множество переходов, so - начальное состояние. Запись a-xа' означает, что (a, x, a') £ Es. Трассой LTS называется последовательность пометок на маршруте, начинающемся в начальном состо-
т.
LTS S обозначим tr(S).
При определении ATS (LTS действий) считается, что задан универсум внешних действий
4 С L. Разрушение будем считать внешним действием 7 £ A. ATS - это такая LTS S = Lts(Vs,Es, so), в которой каждый переход пот,
Es С Vs х (A U {т}) х Vs. Мы будем пис
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.