Семантики взаимодействия с отказами, дивергенцией и разрушением. 2. Условия конечного полного тестирования
Исследуются методы практического тестирования конформности исследуемой системы спецификации. Изучаются практически приемлемые ограничения на семантику, реализацию и спецификацию, а также дополнительные тестовые возможности, которые позволяют проводить полное тестирование за конечное время. Сюда относятся ограничения на размер реализации, возможность наблюдения текущего состояния реализации в процессе тестирования и ограничения на недетерминизм реализации.
Semantics of interactions with refusals, divergence and destruction. 2. Conditions of the final full testing.pdf Статья посвящена методам тестирования соответствия (конформности) иссле-дуемой системы заданным требованиям (спецификации) на основе формальныхмоделей. Эти методы опираются на теорию конформности, которая излагается впредыдущей статье авторов [1]. Основные понятия и обозначения этой теории ис-пользуются в данной работе без повторного определения. Основное вниманиеуделяется возможности применения этой теории на практике. Для этого изучают-ся практически приемлемые ограничения на семантику, реализацию и/или специ-фикацию, а также дополнительные тестовые возможности, которые позволяютпроводить полное тестирование за конечное время. Сюда относятся ограниченияна размер реализации, возможность наблюдения текущего состояния реализации впроцессе тестирования и ограничения на недетерминизм реализации.Проблемы практического тестированияДля практического применения конечными по времени должны быть как гене-рация тестов, так и тестирование по этим тестам. Из первого вытекает конечностьполного набора тестов (или единого теста с рестартом). Для этого «почти» необ-ходимы, хотя и недостаточны, конечность алфавита внешних действий L и конеч-ность LTS-спецификации (числа ее переходов), что на практике вполне приемле-мо. Конечность тестирования опирается на конечность полного набора тестов, ко-нечность времени прогона каждого теста и конечность требуемого числа прого-нов каждого теста.Конечность времени прогона теста гарантируется для конечного теста «прак-тическими предположениями» о семантике: 1) Любая конечная последователь-ность любых действий (как внешних, так и внутренних) совершается за конечноевремя, а бесконечная - за бесконечное время. 2) «Передача» тестового воздейст-вия (нажатие кнопки) в реализацию и наблюдения от реализации выполняются законечное время. Эти предположения гарантируют наблюдение внешнего дейст-вия, выполняемого реализацией, через конечное время после нажатия кнопки,разрешающей это действие.Таким образом, остаются две основные проблемы: 1) конечность полного на-бора тестов и 2) конечность требуемого числа прогонов теста.Эти проблемы не имеют решения в общем виде, поэтому такие решения при-ходится искать в частных случаях: либо ограничивая классы рассматриваемыхспецификаций и/или реализаций, либо предполагая наличие дополнительных тес-товых возможностей, либо сочетая одно с другим. Для первой проблемы одним изтаких практически приемлемых ограничений является конечность реализации,что, как правило, оказывается необходимым, хотя и недостаточным для полногорешения проблемы.Отметим взаимную связь указанных двух проблем. Если число прогонов лю-бых (или некоторых) тестов конечно, то это позволяет применять адаптивное тес-тирование, когда следующие тесты из набора выбираются в зависимости от ре-зультатов, полученных на предыдущих тестах. Например, если после всех прого-нов теста обнаруживается, что после трассы нажатие кнопки P никогда (прилюбых «погодных условиях») не приводит к наблюдению действия zP, то намнет нужды прогонять тесты, построенные по трассам вида ⋅…. Заметим, чтотакого рода отрицательные наблюдения [2] практически невозможны, если нетограничений на число прогонов тестов, так как тогда такие наблюдения могутбыть «вычислены» только после бесконечного числа прогонов тестов.Также взаимосвязаны способы решения проблем: ограничения на классы рас-сматриваемых реализаций и спецификаций напрямую зависят от дополнительныхтестовых возможностей (или их отсутствия). Одной из таких возможностей явля-ется опрос текущего состояния реализации. Если можно «подсматривать» состоя-ния реализации, говорят о тестировании с открытым состоянием, в противномслучае - о тестировании с закрытым состоянием. В следующих разделах мы рас-смотрим эти два вида тестирования и соответствующие ограничения на классыреализаций и/или спецификаций.Проблема конечности требуемого числа прогонов теста общая для этих двухвидов тестирования. Гипотеза о глобальном тестировании дает только теоретиче-скую возможность обнаружить любую ошибку в любой неконформной реализа-ции. На практике нам, прежде всего, требуется конечность различимых «погод-ных условий», а также либо какие-то способы «управления погодой», либо гипо-тезы, ограничивающие возможные проявления недетерминизма реализации. Пер-вое возможно в каких-то частных случаях, например, когда недетерминизм явля-ется следствием псевдопараллелизма, то есть псевдопараллельного выполнениянескольких детерминированных процессов на одном процессоре. Если мы можемвмешиваться в работу планировщика, мы тем самым можем «управлять погодой».Второй способ используется чаще всего в его экстремальном виде, когда ограни-чиваются только детерминированными реализациями (при недетерминированнойспецификации).Здесь мы должны уточнить понятие детерминизма. Обычно LTS-реализацияопределяется как детерминированная, если каждая ее трасса заканчивается ровнов одном состоянии. Однако в общем случае для тестирования в R/Q-семантикедополнительно требуется, чтобы в каждом достижимом состоянии для каждойкнопки PRQ было определено не более одного перехода по действию zP. Этоопределение можно ослабить, если учитывать гипотезу о безопасности, опреде-ляемую спецификацией. В терминах тестов это можно сформулировать так: безо-пасно-тестируемая (удовлетворяющая гипотезе о безопасности) LTS-реализациядетерминирована в R/Q-семантике для заданной спецификации, если каждый тестпри любом его прогоне либо заканчивается только с вердиктом fail в любом со-стоянии реализации, либо только с вердиктом pass в одном и том же состоянииреализации.В данной статье мы исходим из следующей гипотезы о t-недетерминизме: ес-ли в любом состоянии i реализации любую кнопку P нажимать t раз, то реализа-ция продемонстрирует все возможные варианты поведения, то есть будут получе-ны все возможные пары (наблюдение, постсостояние). Эту гипотезу можно осла-бить, если учитывать только те состояния i реализации, которые достижимы побезопасным трассам спецификации, и только те кнопки P, которые безопасны по-сле таких трасс. Кроме того, если любое наблюдение после нажатия кнопки P всостоянии i ошибочно, то можно не налагать никаких ограничений на число такихнаблюдений и постсостояний.Остановимся на одном независимом аспекте проблемы конечности полногонабора тестов: проблеме определения безопасных трасс в спецификации. Дело втом, что правила для отношения безопасности кнопок safe by позволяют послеразличных трасс, заканчивающихся в LTS-спецификации в одном множестве со-стояний (в детерминированной RTS-спецификации - в одном состоянии), по-разному определять безопасные кнопки. При наличии циклов мы получаем беско-нечную цепочку конечных трасс с произвольным распределением безопасныхкнопок после этих трасс. Отношение safe by, при котором трассы, заканчиваю-щиеся в одном множестве состояний LTS-спецификации (в одном состоянии RTS-спецификации), имеют одинаковые множества безопасных после них Q-кнопок(и, тем самым, всех кнопок, поскольку безопасность R-кнопок одинакова для всехтаких трасс), будем называть ограниченным. Это дает нам возможность говоритьо безопасности кнопки P (и соответствующих наблюдений) во множестве S со-стояний LTS-спецификации P safe S (в состоянии s RTS-спецификации P safe s).Для LTS-спецификации с конечным числом состояний конечно число множествсостояний (состояний соответствующей RTS-спецификации). Заметим, что приотсутствии Q-кнопок safe by = safe in и является ограниченным отношениембезопасности.В дальнейшем будем предполагать, что алфавит L (и, тем самым, R/Q-семан-тика), спецификация и реализация конечны, и реализация t-недетерминированная.Обозначим:b - число кнопок,n - максимальное число состояний LTS-реализации,m - максимальное число переходов LTS-реализации, m≤btn,k - максимальное число состояний LTS-спецификации,K - максимальное число состояний RTS-спецификации.Заметим, что для LTS-спецификации с числом состояний k в соответствующейRTS-спецификации K ≤ 2k - 1.Тестирование с закрытым состояниемВ этом разделе рассматриваются наборы примитивных тестов, когда по окон-чанию одного теста выполняется рестарт и запускается другой тест (или тот жесамый тест для следующего прогона). Решение проблемы конечности полного на-бора тестов будем искать двумя способами: сужая классы рассматриваемых спе-цификаций или реализаций. Для конечной семантики по каждой трассе генериру-ется конечное число примитивных тестов (тестов, сгенерированных по однойтрассе спецификации). Поэтому достаточно конечности полного набора трасс, чтодля конечной семантики эквивалентно ограниченности длины трасс полного на-бора.Ограничение на спецификацию. Если число R-кнопок конечно, а в конечнойспецификации нет циклов, то число трасс спецификации конечно, тем более коне-чен полный набор трасс. В то же время не любой цикл приводит к бесконечностиполного набора трасс.Для RTS-спецификации будем называть демоническим состояние s, после ко-торого не бывает ошибок, то есть любая актуальная (встречающаяся в безопасно-тестируемых реализациях) тестовая трасса ⋅, где трасса заканчивается в s, неявляется ошибкой: она имеется в спецификации. Для этого должны быть выпол-нены следующие условия. 1) Определен переход s⎯us` по каждому наблюде-нию u, безопасному в s, за исключением действий, запрещенных петлями по отка-зам, то есть действий zP, где PR и s⎯Ps, и конечное состояние s` также де-моническое. 2) Если это переход по действию uL, то в состоянии s` нет петли поотказу P∅. 3) Если это переход по отказу uR, то в состоянии s` есть петлитолько по отказам Pu и по отказам, по которым есть петли в s. Эти условия неучитывают актуальности тестовых трасс, поэтому в общем случае они только дос-таточны для демоничности состояния s. Для того чтобы эти условия стали такженеобходимыми, требуется пополнение спецификации [4] с последующим удале-нием неактуальных безопасных трасс.Для того чтобы для конечной спецификации в конечном алфавите существо-вал полный набор трасс ограниченной длины, необходимо и достаточно, чтобы вRTS-спецификации любой безопасный маршрут (маршрут с безопасной трассой)не содержал цикла, проходящего через недемонические состояния. Заметим, что вбезопасном маршруте множество состоянийтирования данной реализации I достаточно тестов, которые простые для этой реа-лизации. Для полноты тестирования всех реализаций достаточно, чтобы в набортестов входили все тесты, которые просты для той или иной реализации.Оценим сверху длину N простого теста. Если число состояний реализации I непревосходит n, то, очевидно, N ≤ nK. Если набор тестов состоит из всех тестовдлины не больше nK ≤ n(2k−1), то такой набор тестов содержит все простые тестыдля любой реализации, число состояний которой не больше n. Эта верхняя оценкаявляется точной по порядку: для любых k и n существует семантика с O(k) дейст-виями, LTS-спецификация с O(k) состояниями и неконформная реализация с O(n)состояниями, ошибка в которой не может быть обнаружена тестом длины меньшеO(n2k). Можно показать, что даже для семантики с ограниченным число действийоценка остается суперполиномиальной. В частности, существует семантика сдвумя действиями, для которой в точной верхней оценке показатель степени kзаменяется на cln2k. LTS-спецификации, на которых достигаются эти оценки, су-щественно недетерминированы. Понятно, что для детерминированной LTS-спе-цификации K = k (а не 2k). Однако даже минимальный недетерминизм LTS-специ-фикации (нет -переходов и только в одном состоянии только по одному дейст-вию имеются два перехода в разные состояния) оставляет оценки суперполиноми-альными.Ограничение на недетерминизм реализации. При тестировании с закрытымсостоянием нужна усиленная гипотеза о t-недетерминизме: нас интересует числоT(,P) возможных поведений реализации при нажатии кнопки P не в состоянииреализации (которого мы не видим), а после трассы . Если число состояний реа-лизации ограничено числом n, то T(,P) ≤ tn. Но можно использовать и независи-мую от n гипотезу о том, что T(,P) ограничено некоторым числом T. Такую ги-потезу мы вынуждены использовать, если ограничения налагаются только на спе-цификацию, но не на размер реализации.Оценим сверху число прогонов примитивного теста, который задается чере-дующейся последовательностью кнопок и наблюдений P1,u1,P2,u2,…,PN при за-данном числе T. Последнюю кнопку в тесте мы должны нажимать T раз. Чтобы Tраз гарантированно получить предпоследнее наблюдение uN−1, предыдущуюкнопку PN−1 достаточно нажимать не более T2 раз. Чтобы T2 раз гарантированнополучить наблюдение uN−2, предыдущую кнопку PN−2 достаточно нажимать не бо-лее T3 раз. И так далее. Первую кнопку P1 достаточно нажимать не более TN раз.Тем самым, число прогонов теста оценивается как O(TN). Эта оценка достижимадля некоторых реализаций, но, конечно, для каких-то (классов) реализаций онаможет оказаться гораздо меньше. В частности, для детерминированных реализа-ций оценка O(N).Тестирование с открытым состояниемВ этом разделе рассматривается не набор тестов, а один адаптивный тест свозможными рестартами в середине теста. Будем предполагать, что спецификацияS задана как RTS. Для полноты тестирования нужно проверить все переходы реа-лизации, лежащие на маршрутах с трассами, безопасными в спецификации. Дляэтого LTS-реализация должна быть сильно-связной: из каждого состояния дости-жимо по переходам каждое другое состояние (достаточно ограничиться состоя-ниями, достижимыми из начального состояния по безопасным трассам специфи-кации). Рестарт понимается как одно из внешних действий, отличающихся толькотем, что гарантированно переводит реализацию в начальное состояние. Переходпо рестарту делает трассу пустой. Переходы по рестарту дополнительно учиты-ваются при определении сильно-связности. Также требуется, чтобы начальное со-стояние реализации было стабильным или хотя бы в одном состоянии, достижи-мом по безопасной трассе спецификации, был определен рестарт, безопасный вспецификации после этой трассы. Действительно, в примере на рис.1 реализация вначале тестирования может перейти в состояние 1. После этого без рестарта онапопадет в состояние 0 только после трассы , после которой в спецификациикнопка {y} опасна: ее нельзя нажимать при тестировании. Тем самым ошибка вреализации не будет обнаружена.Рис. 1. РестартПолучая наблюдения и опрашивая состояния реализации, мы будем поэтапностроить реализацию с одновременной проверкой тестируемого условия. Предла-гаемый алгоритм является модификацией алгоритма в [5]. Основные идеи доказа-тельств правильности алгоритма и оценок сложности примерно те же самые и дляэкономии места здесь опущены.Предварительно строятся структуры для спецификации S, которые не зависятот реализации и используются без модификации для верификации любой реали-зации в той же R/Q-семантике. Рассматриваются состояния s в конце безопасныхтрасс, для каждого из которых определяем:A(s)={PRQ|P safe s} - множество кнопок, безопасных в состоянии s;B(s)= (A(s))(RA(s)){} - множество, состоящее из безопасных наблюде-ний и символа ;C(s,u)=s`, где s` состояние после перехода s⎯us` по наблюдению u из со-стояния s; доопределим C(s,)=s. Если таких переходов нет, C(s,u)=∗, где ∗ не сов-падает ни с одним состоянием спецификации.LTS-реализация I строится в процессе тестирования. Более точно: строитсяLTS-модель, имеющая такое же как в реализации множество трасс, безопасных вспецификации, и такое же множество состояний, достижимых по этим трассам.В начале тестирования и после каждого перехода опрашиваем состояние реализа-ции. Переход i⎯zi` по внешнему действию z добавляется, когда после опросасостояния i нажимается кнопка P, после чего наблюдается действие zP, а затемопрашивается постсостояние i`. Если наблюдается отказ с тем же самым пост-состоянием i`=i, то добавляется виртуальный переход-петля по отказу i⎯Pi.Если отказ P наблюдается с другим постсостоянием i`i, то добавляются переходыi⎯i`⎯Pi`. Вместе с каждым переходом по внешнему действию i⎯zi` бу-дем хранить кнопку P(i⎯zi`), нажатие которой вызвало этот переход.При построении I с каждым построенным состоянием i будем связывать мно-жество S(i) состояний спецификации: (i)={S after |Safe(T(S)) & i(I after )}(в детерминированной RTS-спецификации множество S after состояний послетрассы состоит из одного состояния). Множество S(i) состоит из состояний спе-цификации в конце трасс, безопасных в спецификации, имеющихся в реализациии заканчивающихся там в состоянии i. В процессе тестирования будем строитьэти множества S(i), постепенно добавляя в них состояния s`, где {s`}=S after .Кнопка P допустима в i, если она безопасна хотя бы в одном состоянии sS(i).Только допустимые кнопки будут нажиматься в состоянии i. Для каждой допус-тимой кнопки P определим счётчик c(P,i) числа ее нажатий в состоянии i. КнопкаP полна в состоянии i, если: 1) c(P,i)=1 и в I есть виртуальный переход-петля поотказу i⎯Pi или 2) c(P,i)=t. В обоих случаях уже получены все возможные пе-реходы из состояния i при нажатии кнопки P. Состояние полно, если каждая до-пустимая в нем кнопка полна.Кроме S(i) формируются следующие структуры данных для каждого состоя-ния i:A(i)={A(s)|sS(i)} - множество кнопок, допустимых в состоянии i;D(i)={i⎯zi`} - множество переходов из состояния i.Если тестируемое условие выполнено, то должно быть: i⎯ui`D(i)sS(i) uB(s)C(s,u)∗. Мы будем проверять это на каждом шаге тестирования.В начале тестирования после опроса состояния в I есть только одно состояниеi(I after ), где - пустая трасса, и для этого состояния S(i)={s0}, A(i)=A(s0),D(i)=∅ и c(P,i)=0 для каждой допустимой кнопки P.Рис. 2. Общая схема алгоритмаНа рис. 2 изображена общая схема работы алгоритма. Если текущее состояниеполное, то для продолжения тестирования нужно перейти в неполное состояние.Если таких состояний нет, алгоритм заканчивается с вердиктом pass.Рассмотрим переход в неполное состояние. В графе LTS I всегда существуетмножество деревьев, покрывающих все состояния так, что из каждого состояниявыходит не более одного перехода, принадлежащего деревьям, и ориентирован-ных к своим корням, которыми являются все неполные состояния. Выберем лю-бое такое множество деревьев и будем двигаться по его переходам i⎯ui`, на-жимая кнопки P(i⎯ui`). Из-за недетерминизма можем оказаться не в i`, а в дру-гом состоянии i``. Если это не листовое состояние дерева, то в нем определен пе-реход дерева i``⎯ui``` и будем нажимать кнопку P(i``⎯ui```). Доказательстводостижения неполного состояния за конечное число шагов см. в [5].Если текущее состояние i неполное, то выбираем неполную кнопку PA(i),нажимаем ее и получаем один переход i⎯ui` или два перехода i⎯i`⎯Pi`.Постсостояние i` становится новым текущим состоянием. Корректируем счетчикc(P,i). Если получен новый переход, то корректируем I и D(i).После этого выполняется блок «Распространие с верификацией». Для работыэтого блока создается вспомогательный список W всех пар (s, j⎯uj`), где sS(j)и j⎯uj`D(j). В самом начале множество W содержит все пары (s, j⎯uj`) длякаждого нового перехода j⎯uj` и sS(j).Опишем шаг работы блока. Если список W пуст, выходим из блока. Иначе вы-бираем первый элемент (s, j⎯uj`) из списка W, удаляя его из списка. Проверяемтестируемое условие: если j⎯uj`D(j) & uB(s) & C(s,u)=∗, то фиксируетсяошибка и алгоритм заканчивается с вердиктом fail. Если ошибки нет иC(s,u)S(j`), шаг заканчивается. В противном случае добавляем C(s,u) в S(j`) ипомещаем в список W все пары (C(s,u), j`⎯uj``), где j`⎯uj``D(j`); шаг за-канчивается.Отметим, что при таком тестировании верифицируются не только наблюде-ния, полученные после реальных трасс, пройденных при тестировании, но и воз-можные наблюдения после потенциальных трасс, то есть наблюдения и трассы,про которые установлено, что они есть в реализации. Это даёт существенную эко-номию числа тестовых воздействий, необходимых для проверки конформности:мы выполняем множество проверок без реального тестирования, основываясь наполученном знании о поведении реализации. Например, если при тестированииполучены две трассы 1⋅ и 2, где трассы 1 и 2 заканчиваются в реализации водном состоянии i, то мы можем проверить обе трассы: как 1⋅, которую реальнопрошли при тестировании, так и потенциальную трассу 2⋅. Это преимуществодает дополнительная тестовая возможность опроса состояния реализации. По оп-ределению конформности мы должны проверять безопасные (точнее, тестовые)трассы спецификации, имеющиеся в реализации. При тестировании с закрытымсостоянием, получив такую трассу, мы мало что знаем о том, какие еще трассыесть в реализации (гарантированны только те, что получаются из этой трассы уда-лением отказов). При тестировании с открытым состоянием получаем не простотрассу, а маршрут в реализации, то есть трассу с состояниями.Доказательство полноты теста, работающего по описанному алгоритму, анало-гично [5].Приведем оценки сложности алгоритма (доказательство см. в [5]). При тести-ровании обычно наиболее важным считается число тестовых воздействий. ОценкаOT = O(bntn) для t>1, и OT = O(bn2)для t=1. Последняя оценка достигается не толькодля детерминированной реализации, но и во всех случаях, когда переход в непол-ное состояние можно гарантированно выполнить, проходя путь (маршрут без са-мопересечений), длина которого ограничена n. Приведем три таких случая:1. Упомянутый выше случай недетерминизма как следствия псевдопаралле-лизма, когда мы можем вмешиваться в работу планировщика процессов, тем са-мым «управляя погодой».2. Сильно--связные LTS-реализации [3,5]. Это такие LTS, в которых для лю-бой пары состояний i1 и i2 можно в каждом состоянии i найти такую кнопку P(i),что, нажимая только такие кнопки, мы гарантированно окажемся в состоянии i2,хотя путь из i1 в i2, который мы проходим, зависит от недетерминированного по-ведения LTS. Детерминированные LTS - это частный случай сильно--связныхLTS.3. Недетерминизм может быть следствием повышения уровня абстракции примоделировании детерминированной исследуемой системы такой реализацией, ко-торая оказывается недетерминированной в той семантике взаимодействия, кото-рая используется в спецификации. При тестировании связь уровней абстракцииосуществляется промежуточной программой (медиатором). В этом случае принажатии в состоянии i кнопки P медиатор добавляет дополнительный параметр p(возможно, зависящий от i), от которого абстрагируется модель. Если есть воз-можность вместе с наблюдением перехода i⎯ui`, где uP, получить от медиа-тора этот параметр p, то при повторном нажатии в состоянии i кнопки P можносообщить медиатору параметр p, чтобы гарантированно выполнился тот же пере-ход i⎯ui`.Оценка объема вычислений содержит три слагаемых: 1) вычисления, необхо-димые для поиска опрошенного состояния среди пройденных при каждом тесто-вом воздействии, nOT=O(bn2tn) для t>1 или nOT=O(bn3)для t=1; 2) построениемножества деревьев O(b2tn2); 3) вычисления в блоке «Распространение с верифи-кацией» O(mK).ЗаключениеВ данной статье рассмотрены методы тестирования конформности при ограни-чениях на размер семантики, спецификации и реализации, а также при ограничениинедетерминизма реализации. При этих ограничениях эти методы позволяют прово-дить полное тестирование за конечное время. В рамках этих ограничений цельюдальнейших исследований может быть задача минимизации тестового набора.Пополнение спецификации [4] позволяет избавиться от неконформных и неак-туальных безопасных трасс спецификации, тем самым уменьшая множествотрасс, по которым нужно генерировать тесты. Существуют даже курьёзные при-меры нетривиальных спецификаций, в которых бесконечное число безопасныхтрасс, но все они неконформны: без учета неконформности трасс полный набортестов будет бесконечным, а с учетом таких трасс тестирование вообще излишне,так как аналитически доказывается отсутствие конформных реализаций.Для минимизации набора тестов нужно исследовать зависимость между ошиб-ками, когда из наличия в любой безопасно-тестируемой реализации одной ошиб-ки следует наличие в ней другой ошибки. Понятно, что для полноты тестированиядостаточно искать только те ошибки, которые минимальны по этому отношениюследования (это отношение является предпорядком: рефлексивно и транзитивно).Для полноты тестирования достаточно найти хотя бы одну ошибку в некон-формной реализации. В то же время тестирование является лишь этапом в жиз-ненном цикле разработки целевой системы [6]. За тестированием обычно следуютфаза исправления ошибок (в реализации, а иногда и в спецификации) и повторноетестирование. Поэтому для уменьшения числа итераций жизненного цикла можнопоставить задачу исследования методов тестирования, которое должно обнаружи-вать как можно больше ошибок, а также ситуаций, где ошибок нет, чтобы предос-тавить разработчику как можно больше информации. Такое тестирование и соот-ветствующий набор тестов можно называть тотальными. Если полное тестиро-вание выполняется «до первой ошибки», то тотальное - пока не будут обнаруже-ны все имеющиеся в реализации ошибки. Тотальное тестирование является пол-ным, но обратное, вообще говоря, не верно. Для минимизации тотального наборатестов полезно искать только те ошибки, которые неэквивалентны по предпоряд-ку следования ошибок.Другие направления дальнейших исследований могут быть связаны с другимиограничениями на семантику, спецификацию и реализацию и/или с другими до-полнительными тестовыми возможностями.
Скачать электронную версию публикации
Загружен, раз: 309
Ключевые слова
тестирование, конформность, трассы, отказы, недетерминизм, LTS, Testing, conformance, traces, faults, nondeterminism, LTSАвторы
ФИО | Организация | Дополнительно | |
Косачев Александр Сергеевич | Институт системного программирования РАН (г. Москва) | кандидат физико-математических наук, ведущий научный сотрудник | kos@ispras.ru |
Бурдонов Игорь Борисович | Институт системного программирования РАН (г. Москва) | доктор физико-математических наук, ведущий научный сотрудник | igor@ispras.ru |
Ссылки
Кулямин В.В. Технологии программирования. Компонентный подход. М.: Интернет- Университет Информационных технологий; БИНОМ. Лаборатория знаний, 2007. 463 с.
Бурдонов И.Б. Теория конформности для функционального тестирования программных систем на основе формальных моделей: дис. ... д.ф.-м.н. М., 2008. 596 с. URL: http://www.ispras.ru/~RedVerst/RedVerst/Publications/TR-01-2007.pdf
Бурдонов И.Б., Косачев А.С. Полное тестирование с открытым состоянием ограниченно недетерминированных систем // Программирование. 2009. № 6. С. 3−18.
Бурдонов И.Б., Косачев А.С., Кулямин В.В. Формализация тестового эксперимента // Программирование. 2007. № 5. С. 3−32.
Van Glabbeek R.J. The linear time-branching time spectrum II; the semantics of sequential processes with silent moves // Proc. CONCUR '93, Hildesheim, Germany, August 1993 (E. Best, ed.), LNCS 715. Springer-Verlag, 1993. P. 66−81.
Бурдонов И.Б., Косачев А.С. Семантики взаимодействия с отказами, дивергенцией и разрушением. 1. Гипотеза о безопасности и безопасная конформность // Вестник Томского государственного университета. Управление, вычислительная техника и информатика. 2010. № 4(13). С. 124−133.
