|
ИСТИНА |
Войти в систему Регистрация |
ИПМех РАН |
||
Applying Parameterized Model Checking to Real-Life Cache Coherence Protocolsстатья
- Авторы: Burenkov V., Kamkin A.
- Сборник: Proceedings of East-West Design & Test Symposium
- Год издания: 2016
- DOI: 10.1109/EWDTS.2016.7807745
- Аннотация: This paper overviews a technique for verifying cache coherence protocols described in the PROMELA language. The approach is comprised of the following steps. First, a model written for a certain configuration of the memory system is generalized to the model being parameterized with the number of processors. Second, the parameterized model is abstracted from the exact number of processors. Finally, the abstract model is verified with the SPIN model checker in a usual way. The suggested technique has been successfully applied to verification of the MOSI protocol implemented in the Elbrus computer systems.
- Добавил в систему: Камкин Александр Сергеевич