Preview

Вопросы радиоэлектроники

Расширенный поиск

О КОНСЕРВАТИВНОМ ПРЕОБРАЗОВАНИИ ФОРМАЛЬНЫХ МОДЕЛЕЙ, ИСПОЛЬЗУЕМЫХ ПРИМЕНИТЕЛЬНО К МАСШТАБИРУЕМЫМ СИСТЕМАМ ДЛЯ ВЕРИФИКАЦИИ ПРОТОКОЛОВ КОГЕРЕНТНОСТИ ПАМЯТИ

Полный текст:

Аннотация

Приведена математическая модель рассматриваемых протоколов. Предложен метод построения консервативных преобразований модели, используемый при верификации протокола сложной системы на кристалле с архитектурой «Эльбрус».

Об авторе

В. С. Буренков
АО «МЦСТ»; МГТУ им. Н. Э. Баумана
Россия

научный сотрудник, аспирант МГТУ им. Н. Э. Баумана,

АО «МЦСТ», 117105, Москва, ул. Нагатинская, д. 1, стр.23.



Список литературы

1. Буренков, В. С. Анализ применимости формальных методов к верификации протоколов когерентности кэш-памяти масштабируемых систем // Вопросы радиоэлектроники. — 2015. — Сер. ЭВТ. — Вып. 1. — С. 105—116.

2. Буренков, В. С. Анализ применимости инструмента Spin к верификации протоколов когерентности памяти // Вопросы радиоэлектроники. — 2013. — Сер. ЭВТ. — Вып. 3. — С. 126—134.

3. Baier C., Katoen J-P. Principles of Model Checking. — MIT Press, 2008, 984 pp.

4. Holzmann G. The Spin Model Checker: Primer and Reference Manual. — Addison-Wesley Professional, 2003, 608 pp.

5. Clarke E. M., Grumberg O., Peled D. Model Checking. — MIT Press, 1999, 314 pp.


Для цитирования:


Буренков В.С. О КОНСЕРВАТИВНОМ ПРЕОБРАЗОВАНИИ ФОРМАЛЬНЫХ МОДЕЛЕЙ, ИСПОЛЬЗУЕМЫХ ПРИМЕНИТЕЛЬНО К МАСШТАБИРУЕМЫМ СИСТЕМАМ ДЛЯ ВЕРИФИКАЦИИ ПРОТОКОЛОВ КОГЕРЕНТНОСТИ ПАМЯТИ. Вопросы радиоэлектроники. 2016;(3):48-52.

For citation:


Burenkov V. ON CONSERVATIVE TRANSFORMATIONS OF FORMAL MODELS OF CACHE COHERENCE PROTOCOLS USED IN SCALABLE SYSTEMS. Issues of radio electronics. 2016;(3):48-52. (In Russ.)

Просмотров: 12


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2218-5453 (Print)