Аннотация:Описывается метод построения тестовых оракулов для подсистем памяти многоядерных микропроцессоров на основе недетерминированных эталонных моделей. Центральной частью метода является динамическое уточнение вариантов поведения модели на базе реакций, полученных от тестируемой системы. Рассматривается опыт применения предложенного подхода к верификации кэш-памяти L3 микропроцессора «Эльбрус-8С».