Расширение технологии UniTESK средствами генерации структурных тестов Дмитрий Воробьев

"Микроэлектроника и информатика " 2 22 апреля, 2009 г. Функциональная верификация Верификация проверка того, что система функционирует согласно заданным требованиям Верификация критичных систем требует до 70% всех усилий по разработке системы

"Микроэлектроника и информатика " 3 22 апреля, 2009 г. Методы верификации Методы формальной верификации: Обеспечивают полную верификацию На практике их применимость ограничена Методы имитационной верификации (тестирование): Не гарантируют полноты проверки Масштабируются на системы разного уровня сложности Методы полуформальной верификации: Являются подклассом методов имитационной верификации Используют формальные способы для построения тестовых последовательностей и задания требований к системе

"Микроэлектроника и информатика " 4 22 апреля, 2009 г. Технология тестирования UniTESK Использование формальных спецификаций в форме пред- и постусловий Автоматизация проверки правильности поведения на основе формальных спецификаций Автоматизация генерации тестовых последовательностей на основе автоматных моделей

"Микроэлектроника и информатика " 5 22 апреля, 2009 г. Метрики тестового покрытия Разбивают пространство состояний системы и входных воздействий на классы эквивалентности Используются для определения критерия полноты тестирования Классы метрик тестового покрытия Структурные метрики - позволяют обнаружить сложные ошибки, связанные со структурой кода Функциональные метрики - позволяют обнаружить ошибки, связанные с нереализованной функциональностью В технологии UniTESK используются функциональные метрики. Метрики тестового покрытия

"Микроэлектроника и информатика " 6 22 апреля, 2009 г. Недостаток функциональных метрик Реализация на Verilog: module SUM(input A, B, output C) or B) if(A < 0 and B < 0) // 1 ветвь... else // 2 ветвь (не покрыта)... endmodule C

"Микроэлектроника и информатика " 7 22 апреля, 2009 г. UniTESK Генератор структурных тестов Реализация целевой системы Обобщенное тестовое воздействие (ограничения входных данных) Целевая система Спецификация целевой системы Предлагаемый подход UniTESK генерирует обобщенное тестовое воздействие Генератор структурных тестов на основе реализации создает конкретные тестовые воздействия Конкретные тестовые воздействия (наборы конкретных входных данных) Расширенная тестовая система UniTESK

"Микроэлектроника и информатика " 8 22 апреля, 2009 г. Реализация подхода Модуль анализа исходного кода Модуль формирования тестовых воздействий Реализация целевой системы 1 2 Модуль построения данных 3 Модуль передачи тестовых воздействий 1. Анализ кода целевой системы 2. Построение графа потока управления и извлечение путей управления 3. Прием обобщенного тестового воздействия от системы UniTESK 4. Построение конкретных тестовых воздействий 5. Передача тестовых воздействий системе UniTESK Подготовительный этап 4 5 Цикл обработки обобщенного тестового воздействия Система UniTESK

"Микроэлектроника и информатика " 9 22 апреля, 2009 г. Результаты работы Спроектировано расширение инструмента CTESK средствами генерации структурных тестов для Verilog-моделей и разработан прототип Реализация: Анализ структуры реализации: Icarus Verilog Построение конкретных тестовых воздействий: ECLiPSe

"Микроэлектроника и информатика " апреля, 2009 г. Спасибо за внимание! Вопросы?