Использование формальных методов для обеспечения соблюдения программных стандартов

А. И. Гриневич, В. В. Кулямин, Д. А. Марковцев, А. К. Петренко, В. В. Рубанов, А. В. Хорошилов
Труды Института системного программирования РАН

14.11.2006

Страницы: предыдущая :: 1 :: ... :: 3 :: 4 :: 5 :: 6 :: 7 :: следующая

Наиболее глубокие результаты в области формализации стандартов и методик разработки тестов на основе формальных спецификаций получены применительно к телекоммуникационным протоколам. Общий подход к формальному тестированию, представленный в работах [4,7,9] (см. также выше), тоже был разработан в этой области.

Этот подход имеет много общего с представленным в данной статье. Различия связаны, в основном, с необходимостью иметь дело со стандартами большего объема, такими как стандарты POSIX или LSB на интерфейсы библиотек операционных систем. Большой размер стандартов и соответствующих спецификаций приводит к практической невозможности использовать как полные тестовые наборы в терминах работы [9], поскольку они бесконечны, так и выбор набора целей тестирования "на глаз", который является одним из традиционных шагов разработки тестов для телекоммуникационных протоколов. Вместо этого используется более систематическое выделение отдельных требований, понятие критерия тестового покрытия, выбор критерия, ориентированного на учет всех выявленных требований, и генерация тестов, нацеленная на достижение высоких показателей покрытия по выбранному критерию.

Использование контрактных спецификаций также способствует большей практичности и масштабируемости нашего подхода. Программные контракты, с одной стороны, позволяют провести декомпозицию большой системы на более обозримые компоненты, что труднее сделать, используя автоматы или системы переходов, лежащие в основе традиционного формального тестирования. С другой стороны, пред- и постусловия лучше подходят для описания недетерминированного поведения, которое довольно часто вынужден фиксировать стандарт при наличии нескольких возможностей реализовать одну и ту же абстрактную функциональность.

Статья [22] представляет другую попытку формализации стандарта на примере IEEE 1003.5 - POSIX Ada Language Interfaces (интерфейсы POSIX для языка Ada). В рамках описываемого в ней метода на базе требований стандарта сразу строились формальные описания проверяющих их тестов, без промежуточных спецификаций самих требований. Такой метод кажется нам принципиально мало отличающимся от традиционной ручной разработки тестов, при которой разработчик теста читает стандарт, придумывает на основе прочитанного тесты и записывает их в виде некоторых программ.

Более близкий к рассматриваемому в данной статье подход используется в работе [23], где представлены результаты практического использования инструмента автоматизированного создания тестов GOTCHA-TCBeans. Этот инструмент использовался, в частности, для построения тестов для функции fcntl() стандарта POSIX. По ряду идей, касающихся использования формальных техник для тестирования, представленный в [23] подход очень похож на используемый нами, хотя он более сфокусирован на технике создания формальных моделей, чем на обеспечении их адекватности и поддержке прослеживаемости связей между формальными спецификациями и исходным текстом стандарта. Кроме того, используемые в [23] формальные спецификация являются описаниями конечных автоматов на специализированном языке Murφ, а не программными контрактами, как в нашем подходе.

Существует ряд аналогичных работ по разработке тестовых наборов для проверки соответствия стандартам интерфейсов операционных систем. Наиболее известные стандарты в этой области это IEEE Std 1003.1, или POSIX [6], и Базовый стандарт Linux, или LSB [5]. Имеются и наборы тестов на соответствие этим стандартам - это сертификационные тесты POSIX от Open Group [24], открытый проект Open POSIX Test Suite [25], и официальные сертификационные тесты на соответствие LSB [21] от Free Standards Group.

Все эти проекты используют схожие технологии выделения требований из текста стандарта и создания соответствующего каталога требований. После этого тесты разрабатываются вручную на языке C с применением подхода "один тест на одно требование". Они не используют формализацию требований и автоматическую генерацию тестов.

Стоит отметить, что использование подхода "один тест на одно требование" создает предпосылки для укрупнения требований при их выделении, так как велик соблазн проверить как можно больше в одном тесте. К примеру, в тестах Open POSIX мы обнаружили требования, которые включают в себя десяток утверждений, которые в проекте Центра верификации ОС Linux выделяются в отдельные требования. Такое укрупнение требований может приводить к тому, что некоторые утверждения стандарта упускаются из виду и не проверяются, в то время как крупное интегральное требование, в которое они входят, считается протестированным. В результате построенный на основе таких требований отчет об их покрытии может искажать реальное положение дел, утверждая, что все требования стандарта проверены.

Кроме того, автоматическая генерация тестов из спецификаций, используемая в нашем подходе, делает тестовый набор более управляемым, позволяя описывать сами требования стандарта в одном месте, а технику, используемую для их проверки, и тестовые данные - в другом. Это значительно облегчает внесение изменений в тесты при развитии стандарта или их адаптации под требования специфической предметной области.