Инструменты тестирования на основе моделей
Инструменты тестирования на основе моделей с точки зрения их приближения к желательной компонентной архитектуре можно разделить на три группы.
- Традиционные «монолитные» инструменты, использующие специфические языки для оформления моделей. Добавление новых компонентов в них может на практике осуществляться только их разработчиками, а их использование в рамках более широкого инструментария возможно, только если разработчики заранее позаботились о предоставлении подходящего набора интерфейсов.
К инструментам такого типа относятся практически все многочисленные исследовательские прототипные средства тестирования на основе моделей и ряд более стабильных инструментов, использовавшихся во многих разных проектах. В этой второй категории находятся 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 дополняется двумя инструментами: для статической проверки сформулированных ограничений на основе дедуктивного анализа и для их динамической проверки при выполнении методов, ограничения к которым описаны.
