20.02.2014: Выпущен инструментарий LDV Tools 0.5

Опубликовано admin в ЧТ, 20/02/2014 - 08:07

Наиболее значимым изменением в данном релизе является новый менеджер ресурсов, который предназначен для ограничения и подсчета ресурсов, потребляемых инструментами верификации. Новый менеджер ресурсов использует контрольные группы Linux, что позволяет выполнять очень точные измерения без заметных накладных расходов. Также релиз содержит следующие важные изменения:

  • Поддержка автоматической верификации модулей ядра Linux для целевых архитектур, отличающихся от текущей, а также в конфигурациях, задаваемых пользователем.
  • Добавление новой спецификации правила Locking and unlocking SDIO bus.
  • Улучшения существующих спецификаций правил: Module get/put и Block requests.
  • Исправление всех известных ошибок сегментации в Aspectator.
  • Переход на версию 2.7.2 инструмента верификации BLAST.
  • Поддержка CBMC в качестве одного из инструментов, которые могут быть использованы для верификации.
  • Реализация визуализатора трасс ошибок в виде автономного инструмента.

Валидация LDV Tools 0.5 с разными инструментами верификации на 37 известных ошибках в ядре Linux показала, что:

  • BLAST способен выявить 13 из них.
  • CPAchecker способен выявить 11 из них.

По сравнению с LDV Tools 0.4 6 известных ошибок были удалены из валидационного набора, поскольку они не подходят для существующих спецификаций правил, в то время как 5 новых известных ошибок были добавлены в набор (3 благодаря поддержке пользовательских конфигураций, 1 благодаря добавлению новой спецификации правила и 1 благодаря определению подходящей модели окружения). LDV Tools может обнаружить две из этих новых ошибок с помощью инструмента верификации BLAST.

Соответствующий исходный код можно увидеть в репозитории по тэгу v0.5. Инструкции по скачиванию и установке LDV Tools описаны здесь.