Технологии и инструменты Центра верификации ОС Linux
UniTesK: технология тестирования на основе формальных спецификаций
Для формализации стандартов и создания соответствующих тестовых наборов в Центре верификации ОС Linux используется промышленная технология UniTESK, и, в частности, инструменты CTesK. Суть этой технологии заключается в создании формальных спецификаций требований к тестируемой системе и автоматической генерации на основе этих спецификаций соответствующих тестов, проверяющих эти требования. Отличительной чертой технологии UniTESK является разделение собственно спецификаций требований (определяющих правила проверки корректности работы при заданных условиях - состоянии и входных параметрах) и тестовых сценариев (определяющих с какими конкретными входными параметрами и в каком порядке вызывать целевые функции во время тестирования).
CTesK: инструменты поддержки технологии UniTESK для языка C
Подробное описание инструментов CTesK можно найти в следующих документах:
- CTesK 2.2: Руководство пользователя
- CTesK 2.2: Справочник языка спецификации SeC
- CTesK 2.2 для GCC: Быстрое знакомство
- CTesK 2.2 для Microsoft Visual C++® 6.0: Быстрое знакомство
- CTesK 2.2: Инструкция по установке и удалению
Процесс формализации требований и создания тестовых наборов
Технологический процесс создания тестов, используемый в работе Центра верификации ОС Linux, включает следующие основные стадии:
- декомпозиция стандарта на группы связанных функций;
- анализ стандарта и выделение требований для каждой группы;
- формализация проверяемых требований для каждой группы;
- разработка сценариев тестовых воздействий для каждой группы;
- автоматическая генерация тестов инструментами CTesK.