Проект OLVER (Open Linux VERification)

Проект Open Linux VERification (OLVER) был основной активностью Центра верификации Linux в 2005-2006 гг. Главные цели проекта:

  • Проанализировать стандарт Linux Standard Base (LSB) Core 3.1 (ISO/IEC 23360-1) с целью выявления атомарных требований к поведению основных системных библиотек (секции III.Base Libraries и IV.Utility Libraries – всего 1532 функции).
  • Обнаружить неточности и ошибки в тексте стандарта LSB и связанных с ним стандартов и сообщать их оригинальным разработчикам для внесения изменений в будущие версии.
  • Разработать формальные спецификации на языке SeC (спецификационное расширение C), которые будут отражать требования стандарта LSB Core 3.1 для 1532 интерфейсных функций Linux.
  • Разработать открытый тестовый набор для функционального тестирования различных Linux систем на соответствие требованиям стандарта LSB Core в отношении поведения системных интерфейсов прикладного программирования Linux (см. Объект тестирования). Тестовый набор основывается на автоматической генерации тестов из формальных спецификаций требований и соответствующих тестовых сценариев (см. Технологии).
  • Разработать систему конфигурации и запуска тестов. Задача такой системы заключается в предоставлении удобных средств для настройки тестов по ряду параметров (например, глубина тестирования, опции целевой системы, выбор варианта поведения из нескольких, допустимых стандартом) и визуализации результатов тестирования с указанием на расхождения с конкретными требованиями стандарта. Использование такой системы раскрывает потенциал технологии UniTesK по относительно легкой адаптации тестов на различные условия использования (например, для работы в урезанной встраиваемой системе или, наоборот, для учета расширенных требований к корпоративным задачам).

Результаты проекта OLVER опубликованы на сайте Центра и распространяются по свободной лицензии Apache License 2.0.

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