О реализации формального метода верификации масштабируемых систем с когерентной памятью
https://doi.org/10.15514/ISPRAS-2015-27(3)-13
Аннотация
В работе приведен анализ существующих методов верификации протоколов когерентности кэш-памяти масштабируемых систем. На основании литературы изложен формальный метод параметризованной проверки свойств безопасности протоколов когерентности. Предложена архитектура системы верификации протоколов когерентности. Описано применение метода к верификации протокола German, построение и анализ соответствующей Promela-модели. Сформулированы направления по улучшению и автоматизации метода, необходимые для верификации микропроцессоров «Эльбрус».
Ключевые слова
Список литературы
1. Z. Manna, A. Pnueli, “The temporal logic of reactive and concurrent systems: specification,” Springer-Verlag, 427 pp., 1992.
2. E.M. Clarke, O. Grumberg, D. Peled, “Model checking,” MIT Press, 314 pp., 1999.
3. S. Park, D. Dill, “Verification of FLASH cache coherence protocol by aggregation of distributed transactions,” Proceedings of the 8th annual ACM symposium on parallel algorithms and architectures, pp. 288-296, 1996.
4. M. Talupur, “Abstraction Techniques for Parameterized Verification,” PhD Thesis, 2006.
5. E. Clarke, D. Long, K. McMillan, “Compositional model checking,” Proceedings of the fourth IEEE symposium on logic in computer science, 1989.
6. C. Chou, P. Mannava, S. Park, “A simple method for parameterized verification of cache coherence protocols,” Formal methods in computer-aided design, vol. 3312, pp. 382-398, 2004.
7. В.С. Буренков. Генератор тестов для верификации протокола когерентности кэш-памяти // Вопросы радиоэлектроники, серия ЭВТ, 2014, выпуск 3, с. 56-63.
8. G. Holzmann, “The Spin model checker: primer and reference manual,” Addison-Wesley Professional, 608 pp., 2003.
9. S. Krstic, “Parameterized system verification with guard strengthening and parameter abstraction,” Automated verification of infinite state systems, 2005.
10. A. Pnueli, S. Ruah, L. Zuck, “Automatic deductive verification with invisible invariants,” Tools and algorithms for the construction and analysis of systems, vol. 2031, pp. 82-97, 2001.
Рецензия
Для цитирования:
Буренков В. О реализации формального метода верификации масштабируемых систем с когерентной памятью. Труды Института системного программирования РАН. 2015;27(3):183-196. https://doi.org/10.15514/ISPRAS-2015-27(3)-13
For citation:
Burenkov V. On the Implementation of a Formal Method for Verification of Scalable Cache Coherent Systems. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2015;27(3):183-196. (In Russ.) https://doi.org/10.15514/ISPRAS-2015-27(3)-13
Послать статью по эл. почте 