Архитектура среды тестирования на основе моделей

Инструменты тестирования на основе моделей


Инструменты тестирования на основе моделей с точки зрения их приближения к желательной компонентной архитектуре можно разделить на три группы.

  • Традиционные «монолитные» инструменты, использующие специфические языки для оформления моделей. Добавление новых компонентов в них может на практике осуществляться только их разработчиками, а их использование в рамках более широкого инструментария возможно, только если разработчики заранее позаботились о предоставлении подходящего набора интерфейсов.

    К инструментам такого типа относятся практически все многочисленные исследовательские прототипные средства тестирования на основе моделей и ряд более стабильных инструментов, использовавшихся во многих разных проектах. В этой второй категории находятся TorX , TGV , BZ-TT  и Gotcha-TCBeans . Все они основаны на моделировании проверяемой системы в виде различных автоматных моделей. На тех же принципах в целом построены и коммерческие инструменты Conformic Qtronic  и Smartesting Test Designer (ранее Leirios) .

  • Инструменты на основе расширений широко используемых языков программирования, которые сохраняют «монолитность». Примерами являются поддерживающие технологию UniTESK  инструменты CTESK и JavaTESK, а также SpecExplorer , разрабатываемый в Microsoft Research. В обоих случаях для моделирования поведения тестируемых систем используется комбинация из автоматных моделей и контрактных спецификаций.
  • Инструменты, использующие для оформления моделей обычные языки программирования и обладающие рядом характеристик модульности. В частности, эти характеристики включают возможности достаточно легкой интеграции с компонентами от независимых разработчиков и использования самих таких инструментов как части более широкого инструментария.

    Такие инструменты начали появляться не так давно, около 4-5 лет назад. Два наиболее известных примера — это ModelJUnit  и NModel . Похожий инструмент mbt.tigris.org  использует для описания моделей графическую нотацию, поэтому гораздо менее приспособлен для использования в рамках чужих разработок.
    Модели для композиции указываются инструменту построения тестов перечислением имен соответствующих классов.

  • Проверка моделей (model checking). Свойства безопасности проверяются за счет анализа возможности нарушения инвариантов состояний, представленных как методы с особым атрибутом. Свойства живучести могут удостоверяться за счет анализа достижимости стабильных состояний, в которых специально отмеченные характеристические методы возвращают true.


Библиотека CodeContracts предоставляет средства для описания чисто декларативных ограничений на свойства входных параметров и результатов операций. Моделирование состояния не поддерживается. Имеются следующие возможности.


  • Ограничения записываются на языке C# в виде булевских выражений, передаваемых как аргументы библиотечным методам.
  • Можно описывать ограничения следующих видов.


    • Предусловия операций (метод Contract.Requires).
    • Постусловия операций при нормальной работе (Contract.Ensures).
    • Постусловия операций при выдаче исключения (Contract.EnsuresOnThrow).
    • Утверждения о выполнении некоторых свойств в какой-то точке кода внутри метода (Contract.Assert).
    • Инварианты классов — оформляются в виде методов со специальной аннотацией, содержащих обращения к Contract.Invariant.


  • Помимо обычных выражений на C# можно использовать следующие.


    • Кванторные выражения, оформленные в виде обращений к методам Contract.Exists и Contract.ForAll.
    • Обращение к значениям выражений до выполнения проверяемого метода в постусловиях в виде вызова метода Contract.OldValue.
    • Обращение к значению результата в постусловиях с помощью Contract.Result.


  • Библиотека CodeContracts дополняется двумя инструментами: для статической проверки сформулированных ограничений на основе дедуктивного анализа и для их динамической проверки при выполнении методов, ограничения к которым описаны.



Содержание раздела