Применения описанного подхода
Представленный выше подход был успешно использован для формализации и создания наборов тестов для частей стандартов на протоколы IPv6 и IPMP2 [,].
Более масштабным применением этого подхода стал проект Центра верификации ОС Linux [] по формализации Базового стандарта Linux (Linux Standard Base, LSB) [] и разработке тестового набора для проверки соответствия ему. Цель первой фазы проекта - создать формальные спецификации и соответствующий тестовый набор для 1532 функций основных библиотек Linux, перечисленных в разделах III и IV стандарта LSB 3.1 (они описывают базовые библиотеки и библиотеки утилит).
Стандарт LSB задает требования ко многим из этих функций, ссылаясь на уже существующие стандарты. Непосредственно в LSB описывается лишь 15% интерфейсов, большинство - 60% функций - определяются в стандарте Single UNIX Specification [], который включает текущую версию POSIX, а остальные - в таких спецификациях как X/Open Curses [], System V Interface Definition [] и ISO/IEC 9899 (стандарт языка С) []. LSB не включает в себя все эти стандарты, а ссылается лишь на их части, касающиеся описания требований для отдельных функций.
Первая фаза проекта завершится в конце 2006 года. К этому времени планируется сделать все ее результаты доступными в виде открытого кода. В составе этих результатов будет следующее.
- Дополнения к стандарту LSB Core 3.1 в виде формальных спецификаций его требований на расширении языка С (SeC - Specification Extension of С). Такие спецификации выражают требования стандарта в формальном виде, позволяя прояснить нечеткие места в его тексте и сделать явными все подразумеваемые в нем ограничения. Они послужат основой для разработки тестового набора для проверки соответствия стандарту LSB.
- Список замечаний к текстам LSB и связанных стандартов, наработанных в ходе формализации. Это указания на нечеткие, двусмысленные, противоречивые или ошибочные места в стандартах. Они будут направляться разработчикам стандартов для внесения изменений в их будущие версии.
- Тестовый набор для проверки соответствия поведения системных интерфейсов конкретной реализации Linux требованиям стандарта LSB Core 3.1.
Он будет представлять собой набор программ, которые в результате своего выполнения строят HTML-отчеты о проверенных требованиях и найденных несоответствиях.
Тестовый набор будет иметь систему конфигурации, которая позволитнастраивать тесты на особенности конкретной тестируемой системы, допускаемые стандартом, а также установить параметры, определяющие состав тестируемых модулей и глубину тестирования.
