ТЕСТИРОВАНИЕ, ВЕРИФИКАЦИЯ И ВАЛИДАЦИЯ ПРОГРАММ
У л :
ФОРМАЛИЗАЦИЯ ТЕСТОВОГО ЭКСПЕРИМЕНТА-И
© 2013 г. И.Б. Бурдонов, A.C. Косачев
Институт системного программирования РАН 109004 Москва, ул. А. Солженицына, 25 E-mail: igor@ispras.ru, kos@ispras.ru Поступила в редакцию 12.01.2013
Статья развивает подход к тестированию, рассмотренный в [1]. Предлагается формальная модель тестового взаимодействия самого общего вида и конформность типа редукции, для которых зависимость между ошибками практически отсутствует. Показывается, что многие известные конформности в различных семантиках взаимодействия являются частными случаями этой общей модели. Статья посвящена проблеме зависимости между ошибками, определяемыми спецификацией, и связанной с ней проблеме оптимизации тестов. Между ошибками имеется зависимость, если существует такое строгое подмножество ошибок, что любая неконформная реализация (то есть реализация, в которой есть какая-нибудь ошибка) содержит ошибку из этого подмножества. Соответственно, достаточно, чтобы тесты обнаруживали ошибки только из этого подмножества. В предлагаемой общей модели зависимость между ошибками может возникать, когда в качестве класса тестируемых реализаций выбирается то или иное строгое подмножество класса всех реализаций. Частные семантики взаимодействия и/или различные гипотезы о реализации (в частности, гипотезы о безопасности) как раз и предполагают, что тестируемая реализация не любая, а относится к некоторому подклассу (безопасных) реализаций.
1. ВВЕДЕНИЕ
Правильность исследуемой системы в самом широком смысле понимается как её соответствие заданным требованиям. Для верификации (проверки) этого соответствия с помощью формальных методов, объекты и отношения реального мира отображаются в модельные, математические объекты и отношения. Модель исследуемой системы называется реализацией, модель требований - спецификацией, а соответствие требованиям отображается в модельную конформность. Последняя понимается как обычное математическое соответствие, то есть подмножество декартового произведения множеств реализаций и спецификаций.
Спецификация и конформность считаются заданными. Что касается реализации как модели исследуемой системы, то тестовая гипотеза, предполагает, что такая модель существует для каждой исследуемой системы [8].
Если реализация, как модель исследуемой си-
стемы, известна, то возможна статическая (аналитическая) верификация, которая сводится к проверке того, что пара формальных моделей (реализация, спецификация) принадлежит допустимому множеству таких пар, определяемому отношением конформности.
Что делать, если реализация неизвестна (или её слишком сложно построить по исследуемой системе)? В этом случае возникает необходимость в тестировании, которое понимается как динамическая верификация конформности, то есть её проверка в процессе экспериментов. Конечно, для того, чтобы тестирование было возможным, сама конформность должна быть выражена в терминах взаимодействия реализации с окружающей средой. Тест взаимодействует с системой, подменяя собой окружение.
В данной работе мы будем рассматривать не любое тестирование, а только такое, которое основано на трёх предположениях.
Первое предположение. Мы будем рассмат-
ривать только дискретное тестовое взаимодействие, которое сводится к последовательности дискретных событий двух видов: тестовых воздействий на реализацию и наблюдений над поведением реализации. Эту последовательность мы будем называть трассой. Отметим, что в общем случае не всякое поведение реализации может наблюдаться в тестовом эксперименте, то есть в реализации могут происходить события, которые не наблюдаемы и, тем самым, не различимы между собой и не входят в трассу. Такое ненаблюдаемое поведение реализации традиционно обозначается символом т и называется т-активностью.
Дискретное взаимодействие моделируется с помощью, так называемой, машины тестирования, внутри которой находится реализация. Тестовому воздействию соответствует нажатие той или иной кнопки на клавиатуре машины, а наблюдению - появление его символа на экране дисплея. Таким образом, трасса - это последовательность кнопок и наблюдений. Тест понимается как инструкция оператору машины, в которой указывается, что оператор должен делать после той или иной трассы: нажимать кнопки (и какие кнопки) и/или ждать наблюдений.
Всё, что мы можем узнать о реализации с помощью тестирования, - это множество её трасс. Наблюдение в эксперименте некоторой трассы предполагает, что все её префиксы наблюдались в этом же эксперименте в более ранние моменты времени. Поэтому множество трасс реализации префикс-замкнуто. Тестовый эксперимент может быть пустым: ни одна кнопка не нажимается, и наблюдения не ожидаются. В этом случае естественно считать, что наблюдается пустая трасса. Тем самым, в каждой реализации есть пустая трасса, то есть множество трасс реализации не пусто. Поскольку тестовое воздействие (нажатие кнопки) не зависит от самой реализации (оператор в любой момент времени может нажать любую кнопку), продолжение трассы реализации кнопкой также даёт трассу реализации. Это означает, что множество трасс реализации вместе с каждой трассой а содержит и все трассы вида ар, где р - последовательность кнопок.
Спецификацию теперь можно понимать как
описание того, какие множества трасс реализаций правильные (конформные), а какие нет. В общем случае, если реализация имеет множество трасс I, то конформна или неконформна не каждая отдельная трасса а € I, а всё множество трасс I целиком.
Тест (как инструкция оператору) также задаётся непустым префикс-замкнутым множеством трасс. Тестовый эксперимент - это прогон теста, который заканчивается, когда получается максимальная в тесте трасса или "ответвление" в сторону", то есть после некоторой трассы теста получается наблюдение, которым эта трасса не продолжается в тесте. Результатом прогона теста является трасса реализации а € I. Различные прогоны одного и того же теста могут давать разные результаты, если реализация и/или тест недетер минированы.
Тест недетерминирован, если после какой-то трассы теста недетерминировано поведение оператора машины тестирования: он может, как ждать наблюдения, так и нажимать кнопки, или он может только нажимать кнопки, но таких кнопок несколько. Иными словами, тест недетерминирован, если некоторая его немаксимальная трасса продолжается в тесте и наблюдениями, и кнопками, или несколькими кнопками. Недетерминированный тест эквивалентен набору детерминированных тестов в том смысле, что они дают возможность наблюдения одного и того же множества трасс реализации. Поэтому, как правило, рассматривают только детерминированные тесты.
Что касается реализации, то предполагается, что её недетерминизм - это результат абстрагирования от некоторых неучитываемых внешних факторов - погодных условий, которые определяют выбор того или иного поведения детерми-нированны. Гипотеза о глобальном тестировании предполагает, что любые погодные условия могут быть воспроизведены в тестовом эксперименте. Для этого даже детерминированный тест должен прогоняться несколько раз, чтобы наблюдать все возможные для этого теста трассы реализации.
При тестировании выполняется прогон некоторых тестов из некоторого набора тестов при некоторых погодных условиях. Результатом тестирования является множество X трасс, на-
блюдаемых во всех этих тестовых экспериментах. Выносится вердикт pass (проходит) или fail (ошибка). Набор тестов значимый, если каждая конформная реализация его проходит, исчерпывающий, если каждая неконформная реализация его не проходит (обнаруживается ошибка), и полный, если он значимый и исчерпывающий. Заметим, что X - это не обязательно множество всех трасс реализации. Если спецификация утверждает, что любая реализация с большим множеством трасс I 5 X неконформна, то значимый набор тестов может (хотя и не обязан), а полный набор тестов должен выносить вердикт fail X
любого его надмножества). Если спецификация утверждает, что любая реализация с большим множеством трасс I 5 X, наоборот, конформна, то исчерпывающий (и полный) набор тестов может (хотя и не обязан), а полный набор тестов
pass
X
ства).
Второе предположение. В настоящей работе мы ограничимся только теми конформностями, которые отвечают принципу независимости трасс: любая трасса реализации конформна или неконформна независимо от других её трасс. Конформности такого типа называются редукциями. Не является редукцией, например, конформность, которая разрешает реализации иметь как трассу а\, так и трассу а2, но не обе одновременно. Принцип независимости исключает из рассмотрения конформности типа симуляций, которые основаны на соответствии состояний реализации и спецификации, а также конформности, которые требуют обязательного наличия в реализации тех или иных наблюдений после тех или иных трасс.
Для редукции можно считать, что спецификация S (прямо или косвенно) определяет множество разрешаемых трасс tr(S). Если реализа-
I,
означает вложенность I С tr(S) и является частичным (нестрогим) порядком (рефлексивное, симметричное и транзитивное отношение). Трасса а £ tr(S) называется ошибкой.
При тестировании редукции обнаружение любой ошибки а £ I\tr(S) означает, что реализация неконформна. Поэтому значимый набор те-
стов (тест) может (хотя и не обязан) выносить fail а.
для каждой неконформной реализации хотя бы одна имеющаяся в ней ошибка а £ I\tr(S) может быть обнаружена некоторым тестом из набора, то есть является трассой этого теста. Это означает, что неконформность реализации обнаруживается всегда за конечное время, тогда как вывод о конформности реализации может быть сделан, вообще говоря, только после всех прогонов при всех возможных погодных условиях всех тестов полного набора (число таких прогонов может быть бесконечно).
Третье предположение. На практике, естественно, используются только конечные тесты, точнее, тесты, которые заканчиваются за конечное время. При дискретном взаимодействии это означает, что при задании спецификации и генерации тестов используются только конечные трас
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.