Lecture07 (Лекции в ПДФ), страница 2

Существуют методы, позволяющие построить тесты для произвольнойдетерминированной полностью определенной сильно связной спецификации, но размерполучаемых тестов может быть достаточно велик. Такие методы используют установочныепоследовательности (homing sequences).Рассмотрим здесь только один метод, работающий без reset, и предполагающий? Чтоспецификация обладает различающей последовательностью d.Поскольку спецификационный автомат сильно связен, для каждой пары его состояний s1и s2 существует переводящая последовательность стимулов t(s1, s2), выполнение которой в s1переводит автомат в состояние s2.Обозначим для каждого i >= 0 через si’ итоговое состоянием после выполнения d в si.Тогда тест d t(s0’, s1) d t(s1’,s2) d … d t(sn–2’,sn–1) d проверяет, что в реализации для каждогосостояния спецификации есть подобное, в котором d дает ту же последовательность реакций.Чтобы после этого проверить, что некоторый переход работает правильно, нужно перейтив начало перехода si, выполнить его и выполнить d.

Ошибки в реализации могут привести нев начало этого перехода, в другое место. Однако, мы уже знаем, что последовательностьdt(si–1’, si), будучи применена в состоянии si–1, во-первых, проверит, что это действительнотакое состояние с помощью d, а во-вторых, приведет после этого в si уже провереннымспособом. Поэтому, попав в некоторое состояние s, для еще не проверенного перехода si –a->s’ выполним t(s, si–1) d t(si–1’, si) a d.Получаемая таким образом последовательность обеспечит проверку всех переходов.Построим такой тест для нашего примера спецификации.a/xa/xb/x0a/x10b/y2b/xb/yb/ya/ya/x1b/ya/y2Имеем d = ab, s0’ = s2, s1’ = s0, s2’ = s1. Если мы будем обходить состояния в порядке s0-s2s1, то переводящие последовательности пусты. Поэтому первый этап дает abababab, и в егоконце мы оказываемся в состоянии s2.Далее будем проверять переходы в следующем порядке: 1-a->1, 2-a->2, 0-a->0, 1-b->0, 0b->2, 2-b->1.

В этом случае промежуточные переводящие последовательности пусты, заисключением двух последних случаев, поэтому на втором этапе получаем такую входнуюпоследовательность: abaab.abaab.abaab.abbab.babbab.babbab.Итоговый тест:abababab.abaab.abaab.abaab.abbab.babbab.babbab/xyyyxxxy.yyxxx.xyyyy.xxxxy.yyxxy.yxxyyy.xxyyxx.Результат, возвращаемый ошибочной реализацией: xxxxxxxx…, после этого тестированиеможно не продолжать.В этом примере многие ошибки могут быть найдены уже на первом этапе, поскольку вполученную на нем последовательность входят все переходы. Однако, если бы вспецификации имелись переходы по другим символам, отличным от a и b, ошибки в нихобнаруживались бы только на втором этапе.Использование других автоматных моделейДругие автоматные модели — системы размеченных переходов, расширенные иливзаимодействующие автоматы — при их использовании для тестирования чаще всегоприводятся к конечным автоматам.После этого становится можно использовать большое количество методов тестирования,разработанных для конечных автоматов.Литература[1] M.

Broy, B. Jonsson, J.-P. Katoen, M. Leucker, A. Pretschner (eds.). Model Based Testing ofReactive Systems. LNCS 3472, Springer, 2005.[2] В. Б. Кудрявцев, С. В. Алешин, А. С. Подколзин. Введение в теорию автоматов.М.: Наука, 1985.[3] М. П. Василевский. О распознавании неисправностей автоматов. Кибернетика, 9(4):93108, 1973.[4] T. S. Chow. Testing Software Design Modeled by Finite-State Machines.

IEEE Transactions onSoftware Engineering, 4(3):178-187, 1978..