В.С. Буренков, С.Р. Иванов
10
описания метода СМР, и средства, реализующие этот метод, не нахо-
дятся в открытом доступе. В оригинальных статьях [5, 22] упомина-
ется использование языка Murphi для описания моделей. Авторы
настоящей статьи при верификации протоколов используют постоян-
но развивающуюся (в отличие от Murphi) систему Spin, предостав-
ляющую пользователю язык Promela, который нацелен на моделиро-
вание протоколов. Поэтому предполагается адаптация метода к Pro-
mela, для этого, в частности, требуется разработать средство
построения внутреннего представления моделей, пригодного для аб-
страгирования исходной модели и уточнения абстрактной модели.
Также необходимо спроектировать способы представления потоков и
механизмы работы с ними.
ЛИТЕРАТУРА
[1] Pong F., Dubois M. A New Approach for the Verification of Cache Coherence
Protocols.
IEEE Transactions on Parallel and Distributed Systems
, 1995,
vol. 6, no. 8, pp. 773–787.
[2] Буренков В.С. Метод перебора состояний для верификации протоколов
когерентности памяти.
Тр. 54-й науч. конф. МФТИ
, 2011, с. 22, 23.
[3] Pong F., Dubois M. Verification Techniques for Cache Coherence Protocols.
ACM Computing Surveys
, 1997, vol. 29, no. 1, pp. 82–126.
[4] Clarke E., Grumberg O., Peled D.
Model Checking
. MIT Press, 1999, 314 p.
[5] Chou C., Mannava P., Park S. A Simple Method for Parameterized Verifica-
tion of Cache Coherence Protocols.
Formal Methods in Computer-Aided De-
sign
. 2004, vol. 3312, pp. 382–398.
[6] Harrison J. Formal Methods at Intel — An Overview.
Second NASA Formal
Methods Symposium
, 2010. URL:
-
14apr10/slides.pdf (дата обращения 09.11.2013).
[7] Буренков В.С. Инструмент верификации протокола когерентности памя-
ти.
Молодежный научно-технический вестник
, 2013, № 1. URL: http://
sntbul.bmstu.ru (дата обращения 09.11.2013).
[8] Буренков В.С. Анализ применимости инструмента Spin к верификации
протоколов когерентности памяти.
Вопросы радиоэлектроники
, 2013,
вып. 3, с. 126–134.
[9] O’Leary J., Talupur M., Tuttle M. Protocol Verification Using Flows: An Industri-
al Experience.
Formal Methods in Computer-Aided Design
, 2009, pp. 172–179.
[10] Clarke E., Talupur M., Veith H. Environment Abstraction for Parameterized
Verification.
Verification, Model Checking, and Abstract Interpretation
, 2006,
vol. 3855, pp. 126–141.
[11] Talupur M.
Abstraction Techniques for Parameterized Verification,
Thesis …
PhD, 2006. URL:
06-169.pdf (дата обращения 09.11.2013).
[12] Clarke E., Talupur M., Veith H. Proving Ptolemy Right: The Environment Ab-
straction Framework for Model Checking Concurrent Systems.
Proceedings of
the Theory and practice of software, 14th international conference on Tools
and algorithms for the construction and analysis of systems
, 2008, pp. 33–47.
[13] Emerson A., Kahlon V. Reducing Model Checking of the Many to the Few.
Automated Deduction
, 2000, vol. 1831, pp. 236–254.
[14] Emerson A., Kahlon V. Model Checking Large-Scale and Parameterized Re-
source Allocation Systems.
Tools and Algorithms for the Construction and
Analysis of Systems
, 2002, vol. 2280, pp. 251–265.
