Алексей Хорошилов

Кандидат физико-математических наук (2006 г.), тема диссертации - «Спецификация и тестирование компонентов с асинхронным интерфейсом», руководитель А. К. Петренко. С 1999 года работает в Институте системного программирования РАН, на 2011 год — в должности старшего научного сотрудника. С 2009 года работает на кафедре Системного программирования факультета Вычислительной математики и кибернетики МГУ. Основные научные результаты: участие в создании технологии разработки тестов на основе формальных моделей UniTESK и поддерживающих ее инструментов, разработка унифицированной архитектуры тестового набора и правил построения расширений языков программирования для разработки тестов на основе контрактных спецификаций, разработка методов построения тестов для математических библиотек, разработка специализированной технологии быстрого создания тестов работоспособности.

---

Российские операционные системы реального времени.

В докладе рассматриваются отличия операционных систем реального времени (ОСРВ) от операционных систем общего назначения, требования, предъвляемые к ОСРВ, и текущие успехи отечественных разработчиков ОСРВ.

С одной стороны, к ОСРВ предъявляют целый набор дополнительных требований по предсказуемости работы, по безопасности, надежности и т. д. С другой стороны, ОСРВ, в основном, решают задачи управления конкретными системами с применением ограниченной номенклатуры аппаратного обеспечения при помощи ограниченного набора прикладного программного обеспечения. В результате реализация ОСРВ с нуля требует относительно небольших усилий, оцениваемых в десятки человеко-лет, что подтверждают примеры отечественных разработчиков. Но только работающей ОСРВ оказывается недостаточно. Для пользователей требуются документация, инструменты разработки, отладки, конфигурации, верификации и т. д. Сертифицирующие органы требуют пакеты сертификационных документов, включающих требования верхнего и нижнего уровня, тесты, результаты измерений покрытия по коду, анализа свойств безопасности и т. д. В заключении доклада формулируются основные вопросы к разработчикам ОСРВ с точки зрения потенциальных пользователей.

---

• Скачать презентацию в pdf

---

Работа операционной системы лежит в основе функционирования любой компьютерной системы. Сбои и ошибки в операционной системе сказываются на работоспособности системы в целом, поэтому к корректности и надёжности операционных систем предъявляются повышенные требования. Верификация и тестирование операционных систем осложняется целым букетом разнообразных обстоятельств — это и зависимость от аппаратуры, и массированный внутренний параллелизм, и традиционное богатство конфигурационных настроек, и вопросы устойчивости к действиям злоумышленников и к сбоям аппаратуры, и продолжительность непрерывного функционирования.

Опыт ИСП РАН по разработке и применению различных методов верификации операционных систем охватывает следующие направления:
- функциональное тестирование публичного интерфейса ОС;
- систематическое тестирование устойчивости к сбоям ядра ОС;
- статические и динамические методы поиска гонок в ядре ОС;
- статическая верификация модулей ядра ОС Linux;
- дедуктивная верификация компонентов ядра ОС Linux;
- оценка накладных расходов ОС.

Наиболее распространённым подходом к верификации программ является тестирование, то есть динамическая проверка корректности поведения целевой системы в ходе проведения тестового эксперимента. В случае функционального тестирования публичного интерфейса ОС целью эксперимента является проверка того, что наблюдаемое поведение компонентов, доступных через публичные интерфейсы ОС, соответствует декларируемому. Важным моментом для понимания этой задачи является количественная оценка состава интерфейсов ОС. На одной стороне спектра находятся специализированные ОС, предназначенные для работы на встраиваемых устройствах. Например, одна из таких ОС, с которой нам приходилось работать, включает поддержку порядка 700 функций и 80 команд. На другой стороне спектра находятся ОС общего назначения, которые как, например, Debian 7.0 для архитектуры x86, включают в себя более 10 тысяч утилит и более полутора тысяч библиотек, предоставляющих более 700 тысяч функций. Таким образом, задача тщательного функционального тестирования может ставиться только для специализированных ОС или для ключевых интерфейсов ОС общего назначения. Для широкомасштабного функционального тестирования ОС общего назначения приходится использовать методы, в большей степени ориентированные не на достижение высокого качества тестирования, а на обеспечение приемлемых временных и экономических показателей проектов.

Для решения задачи тщательного тестирования отдельных компонентов наш опыт показывает [1], что наиболее эффективным подходом является разработка тестов на основе моделей, в частности, при помощи технологии UniTESK [2], разработанной в ИСП РАН. Также часто для конкретного целевого компонента оказывается наиболее эффективной разработка специализированной тестовой системы. Примером таких систем является набор для тестирования библиотек математических функций [3] и специализированная система тестирования драйверов файловых систем ОС Linux [4].

Примером подхода к решению задачи широкомасштабного тестирования является API Sanity Autotest [5], который позволяет полностью автоматически генерировать тесты работоспособности на основе заголовочных файлов библиотеки и дополнительной семантической информации об особенностях библиотеки, представленных в ней типах данных и специфики их использования в определённых функциях. Типичными примерами такой информации являются описания того:
- как получить корректное значение определённого типа данных;
- каким должно быть корректное значение определённого параметра функции;
- какие проверки можно сделать для возвращаемых значений определённого типа.

В промежутке между тестированием работоспособности и тщательным тестированием находятся более-менее традиционные подходы к построению тестов. Поскольку часто оказывается, что целая группа тестов выполняет приблизительно одни и те же действия, отличающихся лишь в небольшом числе деталей, то естественным развитием традиционного подхода является та или иная форма шаблонов тестов, позволяющая минимизировать дублирование кода. Примером такого развития является технология автоматизированной разработки тестов T2C [6], с помощью которой был разработан набор тестов, проверяющий более 4000 требований стандарта Linux Standard Base (LSB).

В дополнение к функциональному тестированию публичного интерфейса интересной задачей является тестирование, нацеленное на обнаружение специфических видов ошибок: утечки ресурсов, гонки по данным, устойчивости к сбоям. Последнее оказывается в особенности актуально для ядра ОС, которому приходится первому реагировать на сбои в аппаратуре и уметь аккуратно выполнять свои задачи в условиях недостатка ресурсов. Для преодоления ограничений существующих подходов в ИСП РАН разработан метод систематического тестирования устойчивости к сбоям в ядре ОС. Идея метода заключается в выполнении обычного тестового набора, сопровождающегося сбором информации обо всех точках выполнения в коде ядра, в которых возможен сбой или отказ в выделении ресурсов, и автоматическом воспроизведении тестов, приводящих к достижению заданных точек выполнения, с последующей симуляцией сбоя или отказа в выделении ресурсов при одновременном контроле устойчивости системы при обработке этого сбоя. Метод проходит апробацию в проекте по тестированию драйверов файловых систем ОС Linux.

Гонки по данным также являются важной проблемой для ядра ОС [7], поскольку ошибки этого вида очень сложно локализовать и тестировать. В ИСП РАН проводятся исследования сразу над несколькими подходами к обнаружению гонок как при помощи динамических методов KernelStrider [8] и RaceHound [9], так и при помощи статических [10].

Статическая верификация нацелена на выявление типовых ошибок в анализируемом коде посредством умозрительного рассмотрения всех возможных путей выполнения программы без её реального выполнения. В рамках проекта Linux Driver Verification (LDV) [11] в ИСП РАН разрабатывается набор инструментов, реализующих тяжеловесные методы статической верификации, основанные на подходе CEGAR (Counter-Example Guided Abstraction Refinement) [12]. Отличие этого подхода от распространённых инструментов статического анализа (Coverity, Klockwork, SVACE, Smatch, Sparse, Coccinelle) заключается в том, что они позволяют не только найти типовые ошибки, но и доказать их отсутствие. Расплатой за это является то, что тяжеловесные методы требуют на один-два порядка больше времени и памяти. В рамках проекта LDV основной целью является выявление некорректного использования интерфейсов ядра в модулях ядра ОС Linux. Несмотря на наличие большого количества направлений для дальнейшего развития, инструменты LDV уже готовы к применению на практике, что подтверждается тем фактом, что они позволили найти и исправить уже более 180 ошибок в ядре ОС Linux [13].

Если тестирование демонстрирует корректность целевой системы только на определённых тестовых данных и при определённых обстоятельствах, а статическая верификация нацелена только на доказательство отсутствия ошибок определённого вида, то методы дедуктивной верификации позволяют доказать полную корректность целевой системы её функциональным спецификациям, хотя и при определённых предположениях, например, о корректности работы компилятора или о корректности модели внешних сервисов или аппаратуры. Неудивительно, что дедуктивная верификация крайне трудоёмка и применяется только для очень важных компонентов ОС. Интересным опытом ИСП РАН в этом направлении является проект по дедуктивной верификации модуля, реализующего механизм управления доступом в ОС Astra Linux Special Edition.

Отдельной задачей является оценка накладных расходов, которые вносит ОС. И если сравнение накладных расходов разных версий ОС при решении типовых задач не сильно отличается от проведения тестирования, то задача оценки времени выполнения определённых действий, например, времени переключения процессов, близка к задаче проведения физического эксперимента. Как показывает наш опыт разработки измерителей накладных расходов ОСРВ, реализующих стандарт ARINC-653 для получения адекватных результатов приходится учитывать множества факторов, включая поведение компилятора и особенностей используемой аппаратуры.