Обзор результатов Центра верификации ОС Linux
В рамках проекта OLVER получены следующие основные результаты:
- Дополнения к стандарту LSB Core 3.1 в виде формальных спецификаций требований на языке SeC - спецификационном расширении С. Такие спецификации позволяют выразить требования стандарта в формальном виде и при этом прояснить нечеткие места текстовой версии стандарта, а также дополнить ее требованиями, не указанными явно. Данные спецификации интерфейсов ОС Linux служат основой для генерации соответствующих тестов, при этом представляя и самостоятельную ценность как пояснение к тексту стандарта.
- Список обнаруженных во время формализации замечаний к текстам стандарта LSB и нижележащих стандартов. Эти замечания будут включать указания на нечеткие, двусмысленные, противоречивые или ошибочные места в стандартах. Данные замечания будут направляться в соответствующие организации для внесения изменений в будущие версии стандартов.
- Список проблем в компонентах и дистрибутивах ОС Linux, обнаруженных сотрудниками Центра верификации. Найденные проблемы делятся на две основные категории: падения и противоречия в поведении функций требованиям стандарта LSB. Обо всех обнаруженных проблемах мы сообщаем разработчикам, соответствующих компонентов.
- Тестовый набор OLVER, представляющий собой исполняемую программу для нахождения несоответствий поведения (run-time behaviour) прикладных программных интерфейсов системных библиотек конкретной инсталляции Linux требованиям стандарта LSB Core 3.1 (см. объект тестирования).
Результаты работы Центра распространяются по свободной лицензии Apache License 2.0.