УДК: 004.052.32

Разработка верификатора объектов синхронизации драйверов для операционной системы Linux на основе процессной семантики

Ю. П. Кораблин, д-р техн. наук, проф., Российский государственный социальный университет, e-mail: y.p.k@mail.ru, Е. Г. Павлов, аспирант, Российский государственный социальный университет, программист, Исследовательский центр Samsung, e-mail: lucenticus@gmail.com

Описывается инструментальное средство для поиска ошибок в механизмах синхронизации драйверов операционной системы Linux, которое использует метод их обнаружения на основе семантических моделей. Рассматриваемое инструментальное средство позволяет обнаруживать такие ошибки синхронизации как зацикливания, взаимоблокировки, двойные блокировки. Описана процессная семантика объектов синхронизации ядра Linux на языке асинхронных функциональных схем.

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

Стр. 2–9