Linux Driver Verification (LDV)

Linux Driver Verification (LDV)

Программа Linux Driver Verification (LDV) объявлена Центром верификации ОС Linux в июне 2009 года. Основными целями данной Программы являются:
• повышение качества драйверов устройств ОС Linux;
• создание платформы для плодотворного сотрудничества исследователей в области верификации ПО и сообщества разработчиков ядра ОС Linux;
• внедрение передовых инструментов верификации в процесс разработки и сопровождения драйверов устройств.

Для повышения качества драйверов собираются и систематизируются проблемы, возникающие в драйверах устройств, и находятся реальные ошибки в исходном коде. На основе анализа отчетов об ошибках из списка рассылки ядра Linux LKML выделяются часто встречающиеся проблемы. Описание проблем с примерами и ссылками сохраняется в базе правил. Постепенно правила формализуются в виде, который позволяет осуществлять их автоматическую верификацию.

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

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

Исполнитель

Технологии программирования