Semantics of interactions with refusals, divergence anddestruction. Part 1. Hypothesis of safety and safe conformance.pdf Статья посвящена методам тестирования соответствия (конформности) иссле-дуемой системы заданным требованиям (спецификации) на основе формальных моделей. Операционная семантика взаимодействия задаётся с помощью машины тестирования, определяющей тестовые возможности. Выделяется набор теорети-чески достаточно мощных и практически значимых возможностей, сводимый к наблюдению внешних действий и отказов (отсутствие внешних действий). Ново-введениями являются: 1) Параметризация семантики семействами наблюдаемых и ненаблюдаемых отказов, что позволяет учитывать ограничения на (правильное) взаимодействие. 2) Разрушение - запрещённое действие, которое не должно вы-полняться в правильном взаимодействии. 3) Моделирование дивергенции ∆-действием, которого тоже следует избегать в правильном взаимодействии. Пред-лагаются основанные на такой семантике понятие безопасного тестирования, реа-лизационная гипотеза о безопасности и отношение безопасной конформности. В теоретическом плане рассматривается генерация тестов по спецификации в за-данной семантике взаимодействия исследуемого типа.Формализация тестового эксперимента. Семантика взаимодействия и безопасное тестированиеПод «правильностью» исследуемой системы понимается ее соответствие за-данным требованиям. В модельном мире система отображается в реализационную модель (реализацию), требования - в спецификационную модель (специфика-цию), а их соответствие - в бинарное отношение конформности. СпецификацияСемантики взаимодействия с отказами, дивергенцией и разрушением125всегда задана, а существование реализационной модели предполагается (тестовая гипотеза). Если реализация также задана явно, верификация конформности может быть выполнена аналитически. Для реализации, устройство которой неизвестно («черный ящик») или слишком сложно для анализа, применяется тестирование как проверка конформности в процессе тестовых экспериментов. Разумеется, в этом случае требования должны быть функциональными, то есть выражены в терминах взаимодействия системы с окружающим миром, который при тестировании подменяется тестом. Поэтому само отношение конформности и его тестирование основаны на той или иной семантике взаимодействия.Такая семантика формализует тестовые возможности по управлению и наблюдению за поведением тестируемой системы. При тестировании наблюдается только такое поведение реализации, которое, во-первых, «спровоцировано» тестом (управление) и, во-вторых, наблюдаемо во внешнем взаимодействии. Такое взаимодействие моделируется с помощью так называемой машины тестирования [1 - 5]. Она представляет собой «чёрный ящик», внутри которого находится реализация. Управление сводится к тому, что оператор машины, выполняя тест (понимаемый как инструкция оператору), осуществляет тестовое воздействие, нажимая кнопки на клавиатуре машины, тем самым «разрешая» реализации выполнять те или иные действия, которые могут им наблюдаться. Наблюдения (на «дисплее» машины) бывают двух типов: наблюдение внешнего (наблюдаемого) действия, разрешённого оператором и выполняемого реализацией, и наблюдение отказа как отсутствия каких бы то ни было наблюдаемых действий из числа разрешенных нажатыми кнопками. Подчеркнём, что оператор разрешает реализации выполнять именно множество действий, а не обязательно одно действие. Мы предлагаем считать, что оператор может нажимать только одну кнопку, но каждой кнопке соответствует множество разрешаемых действий. После наблюдения (действия или отказа) кнопка отжимается и все внешние действия запрещаются. Далее оператор может нажать другую (или ту же самую) кнопку.Тестовые возможности определяются тем, какие «кнопочные» множества есть на клавиатуре машины и для каких кнопок возможно наблюдение отказа. Тем самым, семантика взаимодействия задается алфавитом внешних действий L и двумя наборами кнопок машины тестирования: с наблюдением соответствующих отказов - семейство Rc2L и без наблюдения отказа - семейство Qc2L. Предполагается, что Rr\Q=… заменена одним переходом s-Д->. Правда, за это приходится расплачиваться наглядностью: не любая детерминированная LTS в таком алфавите является RTS, а лишь та, что удовлетворяет набору условий, определяемых семантикой взаимодействия. При преобразовании LTS в RTS состояниями RTS становятся множества состояний LTS в конце трасс, что аналогично известному алгоритму «детерминизации» порождающего автомата (или графа). Множество трасс LTS или RTS S будем обозначать T(S).Гипотеза о безопасности и безопасная конформностьКак возможно безопасное тестирование, если реализация неизвестна? Например, если в начальном состоянии реализации определено разрушение, то такую реализацию не только нельзя тестировать, но даже запускать на выполнение. Выход в том, чтобы ограничиться реализациями, конформность которых заданной спецификации можно проверить при безопасном тестировании. Это ограничение формулируется как гипотеза о безопасности, и конформность определяется для класса реализаций, удовлетворяющих этой гипотезе. В силу эквивалентности трассовой, LTS- и RTS-моделей достаточно определить гипотезу о безопасности и конформность для трассовых моделей. Такие гипотезу и конформность можно назвать трассовыми, поскольку они зависят только от трасс реализации и спецификации, но не от их состояний и соответствия состояний.Определим формально отношение безопасности «кнопка P безопасна в модели после трассы а». При безопасном тестировании будут нажиматься только безопасные кнопки. Это отношение различно для реализации и спецификации. В полной трассовой реализации I отношение безопасности (safe in) означает, что 1) кнопка P после трассы а неразрушающая: ее нажатие не может означать попытку выхода из дивергенции (трасса не продолжается дивергенцией) и не может вызывать разрушение (после действия, разрешаемого кнопкой), и 2) нажатие кнопки не может привести к ненаблюдаемому отказу (для Q-кнопок): \/P P safe in I after a).130И.Б. Бурдонов, А.С. КосачевЗаметим, что для ioco-семантики мы разрешаем в безопасно-тестируемых реализациях «безопасные» блокировки стимулов после трасс, которые в спецификации этими стимулами не продолжаются. Это более либерально, чем требование всюду определенности реализации по стимулам, предлагаемое автором отношения ioco Яном Тритмансом [8,9]. Этим мы устраняем «несогласованность» отношения ioco, когда конформная всюду определенная по стимулам реализация A и реализация B, отличающаяся от A только наличием «безопасных» блокировок, неразличимы при ioco-тестировании, однако A конформна, а B заведомо не конформна, так как не всюду определена по стимулам и тем самым не входит в домен отношения ioco.Теперь можно определить отношение (безопасной) конформности: реализация I (безопасно) конформна спецификации S, если она безопасна и выполнено тестируемое условие: любое наблюдение, возможное в реализации в ответ на нажатие безопасной (в спецификации) кнопки, разрешается спецификацией:I saco S =def I safe for S & Va e SafeBy(S)r\ IУP safe by S after a obs(a,P,I)cLobs(a,P,S), где obs(a,P,M) =def {u|a-eM & (ueP v u=P & PeR)} - множество наблюдений, которые можно получить над полной трассовой моделью M при нажатии кнопки P после трассы а.Гипотеза о безопасности не проверяема при тестировании, являясь его предусловием; проверяется лишь тестируемое условие. Отношение saco определяет класс конформных реализаций ConfImp(R/Q,S,safe by).Генерация тестовВ терминах машины тестирования тест - это инструкция оператору машины. В каждом пункте инструкции указана кнопка, которую оператор должен нажимать, и для каждого наблюдения - пункт инструкции, который должен выполняться следующим, или вердикт (pass или fail), если тестирование нужно закончить. В тесте после кнопки P допускается только такое наблюдение u, которое разрешается кнопкой P, то есть ueP v u=PeR.Тест задается префикс-замкнутым множеством конечных историй, в котором 1) каждая максимальная история заканчивается наблюдением, и ей приписан вердикт; 2) после каждой немаксимальной истории, заканчивающейся кнопкой, следуют только те наблюдения, которые разрешаются этой кнопкой, и обязательно следуют те из них, что встречаются в безопасно-тестируемых реализациях после подтрассы этой истории.Тест безопасен тогда и только тогда, когда в каждой его истории каждая кнопка безопасна в спецификации после подтрассы непосредственно предшествующего этой кнопке префикса истории. Иными словами, тест безопасен, если подтрассы его историй являются тестовыми, где тестовая трасса - это безопасная трасса или трасса а-, где трасса а безопасна в спецификации, а наблюдение u безопасно после а в спецификации (но не обязательно имеется в ней). Достаточно ограничиться только актуальными тестовыми трассами, под которыми понимаются трассы, встречающиеся в безопасно-тестируемых реализациях. В частности, трасса должна быть согласованной, хотя в спецификации могут быть согласованные, но неактуальные тестовые трассы.Реализация проходит тест, если её тестирование этим тестом всегда заканчивается с вердиктом pass. Реализация проходит набор тестов, если она проходитСемантики взаимодействия с отказами, дивергенцией и разрушением131каждый тест из набора. Набор тестов значимый, если каждая конформная реали-зация его проходит; исчерпывающий, если каждая неконформная реализация его не проходит; полный, если он значимый и исчерпывающий. Для определения конформности любой безопасно-тестируемой реализации ставится задача генера-ции полного набора тестов по спецификации.Полный набор тестов всегда существует, например, им является набор всех примитивных тестов [2]. Такой тест строится по немаксимальной (по отношению «является префиксом») безопасной R-трассе спецификации. Для этого в трассу вставляются кнопки: перед отказом R - кнопка R, перед действием z - любая кнопка P, разрешающая действие z и безопасная после соответствующего префик-са трассы, а после всей трассы - любая безопасная после нее кнопка P`. Безопас-ность трассы гарантирует безопасность кнопки R и наличие безопасной кнопки P, а немаксимальность трассы (среди безопасных) гарантирует наличие последней кнопки P`. Выбор кнопок, вообще говоря, неоднозначен: по одной безопасной трассе спецификации генерируется множество примитивных тестов. Однако мно-жества тестов, сгенерированных по разным трассам, не пересекаются.Если наблюдение, полученное после нажатия кнопки, продолжает трассу, тест продолжается (немаксимальная в тесте история). Наблюдение, полученное после нажатия последней кнопки, и любое наблюдение, «ответвляющееся» от трассы, всегда заканчивают тестирование (максимальная в тесте история). Вердикт pass выносится, если полученная R-трасса (подтрасса максимальной истории) есть в спецификации, а вердикт fail - если нет. Такие вердикты соответствуют строгим тестам, которые, во-первых, значимые (не фиксируют ложных ошибок) и, во-вторых, не пропускают обнаруженных ошибок.Любой строгий тест как множество историй равен объединению некоторого множества примитивных тестов, то есть они обнаруживают те же самые ошибки. Поэтому можно ограничиться только примитивными тестами. Но и среди прими-тивных тестов могут быть заведомо «лишние». Например, достаточно генериро-вать тесты только по трассам, в которых нет повторных (не разделенных дейст-виями) отказов: если наблюдается отказ P, то повторное нажатие кнопки P гаран-тированно дает отказ. Кроме того, в спецификации могут быть безопасные некон-формные трассы, то есть трассы, которые не могут встречаться в конформных реализациях.Как сказано выше, в любой момент времени реализация выполняет любое внешнее действие, которое определено в ней и разрешено оператором, или любое внутреннее действие. Если таких действий несколько, выбирается одно из них не-детерминированным образом. Предполагается, что недетерминизм реализации -это явление уровня абстракции, которое определяется тестовыми возможностями по наблюдению и управлению, то есть семантикой взаимодействия. Иными сло-вами, поведение реализации недетерминировано, поскольку оно зависит от неких не учитываемых факторов - «погодных условий», которые определяют выбор вы-полняемого действия детерминировано. Для того чтобы тестирование было пол-ным, любые погодные условия должны быть воспроизводимы в тестовом экспе-рименте, причём для каждого теста. Если это так, то есть при бесконечной после-довательности прогонов теста проявятся все возможные погодные условия, тести-рование называется глобальным [5]. Мы абстрагируемся от количества вариантов погодных условий, здесь важна лишь потенциальная возможность проверить по-ведение системы при любых погодных условиях и любом поведении оператора. Без этого мы не можем быть уверены, что провели тестовые испытания каждого132И.Б. Бурдонов, А.С. Косачевтеста для всех возможных погодных условий, то есть при любом возможном не-детерминированном поведении реализации.Если гипотеза о глобальном тестировании верна, то для того, чтобы тесты можно было прогонять при всех возможных погодных условий, набор тестов должен быть перечислим. Тогда тесты прогоняются по мере их перечисления так, чтобы каждый перечисленный тест прогонялся неограниченное число раз в «диа-гональном» процессе перечисления тестов и последовательности прогонов каждо-го теста. Поскольку все тесты конечны, каждый из них заканчивается через ко-нечное время, после чего выполняется рестарт системы, и прогоняется следую-щий тест или повторно один из уже перечисленных тестов. Если реализация не-конформна, то полнота набора тестов гарантирует обнаружение ошибки через ко-нечное время. Однако конформность реализации не может быть обнаружена за конечное время, если набор тестов бесконечен или глобальное тестирование тре-бует не конечного, а бесконечного числа прогонов тестов. Но это уже проблема практического тестирования.Отметим, что последовательность прогонов тестов, чередующихся с рестартом системы, можно рассматривать как один тест, в котором, кроме тестовых воздей-ствий, встречается рестарт системы. Вместо конечности каждого теста в наборе тестов мы должны потребовать конечность каждого отрезка единого теста между рестартами, то есть отсутствие в нем бесконечного постфикса без рестарта. Пред-полагается, что рестарт системы всегда выполняется правильно (система действи-тельно «сбрасывается» в начальное состояние), и его не нужно тестировать. Тем самым, различие между перечислимым набором тестов и одним тестом с рестар-тами условное и определяется удобством организации тестирующей системы.ЗаключениеПредлагаемые в статье параметризованная R/Q-семантика взаимодействия, ги-потеза о безопасности, безопасная конформность и метод генерации тестов со-ставляют основу теории конформности [2], которая обобщает многие встречаю-щиеся в литературе и используемые на практике конформности и методы их тес-тирования. В частности, failure trace semantics [3, 4, 6 - 8, 12] и семантика попу-лярного отношения ioco [8,9] являются частными случаями R/Q-семантики. В на-стоящее время эта теория развита в нескольких направлениях. 1) Пополнение спецификации, решающее проблему нерефлексивности спецификации по отно-шению конформности, а также проблему безопасных неконформных и тестовых неактуальных трасс спецификации [2]. 2) Монотонное преобразование специфи-кации, решающее проблему верификации имеющейся спецификации системы (её согласованности со спецификациями компонентов), и проблему генерации спе-цификации системы по спецификациям компонентов [2]. 3) Введение в модель приоритетов и соответствующая модификация конформности и генерации тестов [10]. 4) Распространение предлагаемого подхода на симуляции - конформности, основанные не только на трассах наблюдений, но и на соответствии состояний реализации и спецификации [13]. Также исследованы вопросы эквивалентности семантик взаимодействия [14] и преобразования семантик при тестировании с ис-пользованием программ-медиаторов, осуществляющих преобразование тестовых воздействий и наблюдений [15].Другого рода исследования связаны с применением этой теории на практике. Основная задача, решаемая здесь, - это поиск практически приемлемых ограни-Семантики взаимодействия с отказами, дивергенцией и разрушением133чений на семантику, реализацию и/или спецификацию, а также дополнительных тестовых возможностей, которые позволяли бы проводить полное тестирование за конечное время. Сюда относятся ограничения на размер реализации, возможность наблюдения текущего состояния реализации в процессе тестирования и ограниче-ния на недетерминизм реализации [13, 15, 16].

Скачать электронную версию публикации