Методика параметризованной верификации протоколов когерентности памяти
https://doi.org/10.15514/ISPRAS-2017-29(4)-15
Аннотация
Список литературы
1. Patterson D.A., Hennessy J.L. Computer Organization and Design: The Hardware/Software Interface. Morgan Kaufmann, 2013. 800 p.
2. Sorin D.J., Hill M.D., Wood D.A. A Primer on Memory Consistency and Cache Coherence. Morgan and Claypool, 2011. 195 p.
3. Clarke E.M., Grumberg O., Peled D.A. Model Checking. MIT Press, 1999. 314 p.
4. Буренков В.С. Анализ применимости инструмента Spin к верификации протоколов когерентности памяти. Вопросы радиоэлектроники. Сер. ЭВТ. 2014. Вып. 3. стр. 126-134.
5. Burenkov V.S., Kamkin A.S. Checking Parameterized PROMELA Models of Cache Coherence Protocols. Trudy ISP RAN/Proc. ISP RAS. vol. 28, issue 4, 2016, pp. 57-76. DOI: 10.15514/ISPRAS-2016-28(4)-4
6. Буренков В.С., Камкин А.С. Метод масштабируемой верификации PROMELA-моделей протоколов когерентности кэш-памяти. Сб. трудов VII Всероссийской научно-технической конференции «Проблемы разработки перспективных микро- и наноэлектронных систем». 2016. Часть II. стр. 54-60.
7. Burenkov V.S., Kamkin A.S. Applying Parameterized Model Checking to Real-Life Cache Coherence Protocols. Proc. of IEEE East-West Design & Test Symposium. 2016. pp. 1-4.
8. Буренков В.С., Иванов С.Р. Метод построения абстрактных моделей, используемых для верификации протоколов когерентности кэш-памяти. Вестник МГТУ им. Н.Э. Баумана. 2017, вып. 1, стр. 49-66.
9. McMillan K. Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking. Conference on Correct Hardware Design and Verification Methods, 2001. pp. 179-195.
10. Chou C.-T., Mannava P.K., Park S. A Simple Method for Parameterized Verification of Cache Coherence Protocols. Formal Methods in Computer-Aided Design, 2004. LNCS, Vol. 3312, pp. 382-398.
11. Krstic S. Parameterized System Verification with Guard Strengthening and Parameter Abstraction. International Workshop on Automated Verification of Infinite-State Systems, 2005.
12. Talupur M., Tuttle M.R. Going with the Flow: Parameterized Verification Using Message Flows. Formal Methods in Computer-Aided Design, 2008. pp. 1-8.
13. O'Leary J., Talupur M., Tuttle M.R. Protocol Verification Using Flows: An Industrial Experience. Formal Methods in Computer-Aided Design, 2009. pp. 172-179.
14. Baier C., Katoen J.-P. Principles of Model Checking. The MIT Press. 2008. 984 p.
15. de Guzman, J. Fastest numeric parsers in the world! http://boost-spirit.com/home/2014/09/03/fastest-numeric-parsers-in-the-world/.
16. Spin Version 6 - Promela Grammar. http://spinroot.com/spin/Man/grammar.html.
17. Holzmann, G. The Spin Model Checker: Primer and Reference Manual. Addison-Wesley. 2004. 608 p.
Рецензия
Для цитирования:
Буренков В.С. Методика параметризованной верификации протоколов когерентности памяти. Труды Института системного программирования РАН. 2017;29(4):231-246. https://doi.org/10.15514/ISPRAS-2017-29(4)-15
For citation:
Burenkov V.S. A Technique for Parameterized Verification of Cache Coherence Protocols. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2017;29(4):231-246. https://doi.org/10.15514/ISPRAS-2017-29(4)-15
Послать статью по эл. почте 