Preview

Труды Института системного программирования РАН

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

Подход к построению тестовых оракулов для подсистем памяти многоядерных микропроцессоров на основе моделей

https://doi.org/10.15514/ISPRAS-2015-27(3)-11

Аннотация

В работе представлен метод построения тестовых оракулов для подсистем памяти многоядерных микропроцессоров. В методе используется недетерминированная эталонная модель тестируемой системы. Идея подхода состоит в динамическом уточнении поведения модели на основе реакций, полученных от системы. При возникновении недетерминированного выбора в эталонной модели создаются и запускаются дополнительные экземпляры модели, каждый из которых моделирует возможный вариант поведения. При получении реакции от тестируемой системы завершаются экземпляры модели, для которых данная реакция является некорректной. Признаком ошибки является отсутствие активных экземпляров эталонной модели. Предложенный метод использовался для верификации кэш-памяти третьего уровня микропроцессора «Эльбрус-8C»; с его помощью было найдено три ошибки.

Об авторах

Александр Камкин
ИСП РАН
Россия


Михаил Петроченков
ЗАО «МЦСТ»
Россия


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

1. Sorin D.J., Hill M.D., Wood D.A. A Primer on Memory Consistency and Cache Coherence. Morgan and Claypool, 2011. 195 p.

2. А. Камкин, М. Петроченков. Система поддержки верификации реализаций протоколов когерентности с использованием формальных методов // Вопросы радиоэлектроники, сер. ЭВТ. 2014, вып. 3, с. 27-38.

3. Bergeron J. Writing Testbenches: Functional Verification of HDL Models. Kluwer Academic Publishers, 2000. 354 p.

4. von Bochmann G., Haar S., Jard C., Jourdan G.V. Testing Systems Specified as Partial Order Input/Output Automata. ICTSS, 2008. p. 169-183.

5. Kuliamin V., Petrenko A., Pakoulin N., Kossatchev A., Bourdonov I. Integration of Functional and Timed Testing of Real-Time and Concurrent Systems. PSI, 2003. p. 450-461.

6. Chupilko M., Kamkin A. Runtime Verification Based on Executable Models: On-the-Fly Matching of Timed Traces. MBT, EPTCS 111, 2013, p. 67-81.

7. Баратов Р.А., Камкин А.С., Майорова В.М., Мешков А.Н., Сортов А.А., Якушева М.А. Трудности модульной верификации аппаратуры на примере буфера команд микропроцессора «Эльбрус-2S» // Вопросы радиоэлектроники, сер. ЭВТ, 2013, вып. 3. с. 84-96.

8. Кожин А.С., Кожин Е.С., Костенко В.О., Лавров А.В. Кэш третьего уровня и поддержка когерентности микропроцессора «Эльбрус-4С+» // Вопросы радиоэлектроники, сер. ЭВТ, 2013, вып. 3. с. 26-38.


Рецензия

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


Камкин А., Петроченков М. Подход к построению тестовых оракулов для подсистем памяти многоядерных микропроцессоров на основе моделей. Труды Института системного программирования РАН. 2015;27(3):149-160. https://doi.org/10.15514/ISPRAS-2015-27(3)-11

For citation:


Kamkin A., Petrochenkov M. A Model-Based Approach to Design Test Oracles for Memory Subsystems of Multicore Microprocessors. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2015;27(3):149-160. (In Russ.) https://doi.org/10.15514/ISPRAS-2015-27(3)-11



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


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)