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

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

14.11.2006

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

Представленный выше подход был успешно использован для формализации и создания наборов тестов для частей стандартов на протоколы IPv6 и IPMP2 [11,14].

Более масштабным применением этого подхода стал проект Центра верификации ОС Linux [15] по формализации Базового стандарта Linux (Linux Standard Base, LSB) [5] и разработке тестового набора для проверки соответствия ему. Проект был назван OLVER - Open Linux Verification. Цель первой фазы проекта - создать формальные спецификации и соответствующий тестовый набор для 1532 функций основных библиотек Linux, перечисленных в разделах III и IV стандарта LSB 3.1 (они описывают базовые библиотеки и библиотеки утилит).

Стандарт LSB задает требования ко многим из этих функций, ссылаясь на уже существующие стандарты. Непосредственно в тексте LSB описывается лишь 15% интерфейсов, большинство - 60% функций - определяются в стандарте Single UNIX Specification [6], который включает текущую версию POSIX, а остальные - в таких спецификациях как X/Open Curses [16], System V Interface Definition [17] и ISO/IEC 9899 (стандарт языка C) [18]. LSB не включает в себя все эти стандарты, а ссылается лишь на их части, касающиеся описания требований для отдельных функций. Всего, вместе со стандартами, на которые он ссылается, LSB состоит из более чем 6000 страниц текста.

Первая фаза проекта завершится в конце 2006 года. Все ее результаты будут доступны в виде открытого кода на сайте проекта [15]. В составе этих результатов будет следующее.

• Дополнения к стандарту LSB Core 3.1 в виде формальных спецификаций его требований на расширении языка С (SeC - Specification Extension of C). Такие спецификации выражают требования стандарта в формальном виде, позволяя прояснить нечеткие места в его тексте и сделать явными все подразумеваемые в нем ограничения. Они послужат основой для разработки тестового набора для проверки соответствия стандарту LSB.

• Список замечаний к текстам LSB и связанных стандартов, наработанных в ходе формализации. Это указания на нечеткие, двусмысленные, противоречивые или ошибочные места в стандартах. Они будут направляться разработчикам стандартов для внесения изменений в их будущие версии.

• Тестовый набор для проверки соответствия поведения системных интерфейсов конкретной реализации Linux требованиям стандарта LSB Core 3.1. Он будет представлять собой набор программ, которые в результате своего выполнения строят HTML-отчеты о проверенных требованиях и найденных несоответствиях. Тестовый набор будет иметь систему конфигурации, которая позволит настраивать тесты на особенности конкретной тестируемой системы, допускаемые стандартом, а также установить параметры, определяющие состав тестируемых модулей и глубину тестирования.

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

За первые 3 месяца работы были проспецифицированы и снабжены базовыми тестовыми сценариями 320 функций из 41 группы. В процессе формализации было выделено около 2150 отдельных требований стандарта к этим функций. При этом к некоторым функциям предъявляется всего лишь несколько требований, в то время как к другим - несколько десятков.

На 1 июня 2006 года проанализирован текст стандарта, касающийся 930 функций. Выделено 10500 элементарных требований. Из этих функций для 740 разработаны формальные спецификации и тесты. Полученный на это момент набор спецификаций и тестов содержит около 400 тысяч строк кода. Текущее состояние проекта отражается на сайте [15].

Качество разрабатываемых тестов определяется исходя из покрытия требований, но сравнить по этой характеристики несколько различных тестовых наборов для тестирования функциональности достаточно тяжело, в них почти всегда элементарные требований выделяются по-разному (см. далее). Если же сравнивать покрытие кода для некоторых групп функций, можно отметить, что полученный в этом проекте тестовый набор дает большее покрытие, чем другие известные наборы для тестирования функциональности. Получаемое покрытие кода приближается к результатам отладочного тестового набора для библиотеки glibc [19], созданного ее разработчиками, обладающими детальными знаниями об особенностях реализации различных ее функций, и не нацеленного на проверку соответствия каким-либо стандартам. Результаты сравнения покрытия кода для некоторых групп функций для тестовых наборов LTP [20], официального тестового набора LSB [21], отладочного тестового набора glibc [19] и набора, полученного в рассматриваемом проекте, приведены в Таблице 1.

На основе достигнутой производительности можно утверждать, что первая фаза проекта потребует около 15 человеко-лет. Чтобы начать работать в этом проекте, опытному разработчику программного обеспечения (не обычному тестировщику!) требуется около месяца для обучения особенностям технологии и изучения сопутствующих процессов. Полученные предварительные результаты позволяют надеяться, что рассмотренный подход может успешно применяться для проектов такого масштаба.

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