Динамическая верификация, основанная на исполнимых моделях: сравнение временных трасс времени исполнения.
Динамическая верификация, основанная на исполнимых моделях: сравнение временных трасс времени исполнения.
Авторы
Аннотация
Динамическая верификация – это проверка того, что исполнение системы удовлетворяет или нарушает данное свойство корректности. Процедура, которая автоматически, а обычно в процессе исполнения, проверяет соответствие поведения системы определенному свойству, называется монитором. В настоящее время для выражения свойств наблюдаемого поведения вычислительных систем используется множество формализмов, а также множество формализмов были предложены для создания мониторов. Однако частой является ситуация, когда сложные формализмы и методы не нужны, так как доступна исполнимая модель системы. Изначальная цель и структура модели не важны: необходимо лишь, чтобы тестируемая система и ее модель имели схожие наборы интерфейсов. В этом случае функция монитора осуществляется следующим образом: два «черных ящика», система и ее эталонная модель, запускаются параллельно, и на них подаются одни и те же тестовые последовательности; монитор динамически получает их выходные трассы и пытается их сравнить. Основная проблема здесь заключается в том, что модель обычно более абстрактна, чем реальная система в смысле функциональности и привязки к синхросигналу. Следовательно, прямое сравнение трасс не должно осуществляться, что позволяет событиям системы возникать в некотором отличном от модели порядке или даже некоторым из них отсутствовать. В данной статье изучается отношение соответствия времени исполнения для временных систем (т.е. таких систем, где входные и выходные сигналы распределены вдоль временных осей). В статье также предлагается ориентированная на практическое применение методология создания и настройки мониторов для временных систем, основанная на исполнимых моделях. Методология была успешно применена в ряде промышленных проектов по динамической верификации аппаратуры.
Полный текст статьи в формате pdf (на английском)Издание
Model-Based Testing Workshop (MBT), 2013. Стр. 67-81.
DOI: 10.4204/EPTCS.111.6
Научная группа
Все публикации за 2013 год
Все публикации