Личный кабинет
Подробное описание документа
Буренков В. С.
Метод построения абстрактных моделей, используемых для верификации протоколов когерентности кэш-памяти масштабируемых систем / Буренков В. С., Иванов С. Р. - DOI 10.18698/0236-3933-2017-1-49-66 // Вестник МГТУ им. Н. Э. Баумана. Сер. Приборостроение. - 2017. - № 1. -
Скачать документ
Изложен новый подход к решению задачи верификации протоколов когерентности кэш-памяти масштабируемых микропроцессорных систем. Рассмотрена математическая модель протоколов когерентности. Модель представляет собой отдельные группы устройств, работающих в соответствии с протоколом, в виде графов программ, а протокол в целом - в виде канальной системы, из которой может быть получена и исследована методом Model checking система переходов. Предложен подход к описанию моделей протоколов когерентности на языке Promela и сформулированы ограничения на модели. Представлен метод построения абстрактных моделей, позволяющий существенно уменьшить их размер и базирующийся на преобразованиях отдельных графов программ исходной модели, или на синтаксических преобразованиях Promela-процессов. Приведено математическое доказательство сохранения преобразованиями свойств-инвариантов. Результаты основаны на практике верификации протокола сложной системы на кристалле с архитектурой "Эльбрус".
004.052.42 Обнаружение ошибок.
Статья опубликована в следующих изданиях
№ 1. - 2017.
