?
Комбинаторная генерация тестовых программ для микропроцессоров на основе формальных спецификаций системы команд
Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС). 2016. Т. II. С. 38–45.
Татарников А. Д.
Генерация тестовых программ и анализ результатов их симуляции на проектной модели являются основным подходом к функциональной верификации микропроцессоров. Верификация – крайне трудоемкий процесс. По некоторым оценкам затраты на нее составляют около 70% от общих трудозатрат на разработку микропроцессора. Это связано с тем, что логика работы современных микропроцессоров содержит огромное количество состояний, и для того, чтобы обеспечить их полное покрытие, требуются значительные усилия. В данной работе рассматривается подход к генерации тестовых программ, который позволяет повысить эффективность тестирования за счет использования комбинаторных методов для генерации тестовых программ. Основная идея метода состоит в построении тестовых воздействий путем комбинаторного перебора инструкций микропроцессора и ситуаций в их работе, условия возникновения которых заданы в виде ограничений. Знание о системе команд микропроцессора автоматически извлекается из формальных спецификаций.
Научное направление:
Компьютерные науки
Приоритетные направления:
компьютерно-математическое
Язык:
русский
Татарников А. Д., Камкин А. С., Проценко А. С. и др., Труды Института системного программирования РАН 2016 Т. 28 № 6 С. 87–102
ARM — это семейство микропроцессорных архитектур, разработанных в одноименной компании. Новейшая архитектура этого семейства, ARMv8, содержит большое число команд разных типов и отличается сложной организацией виртуальной памяти (включающей аппаратную поддержку многоуровневой трансляции адресов и виртуализации); все это делает функциональную верификацию микропроцессоров этой архитектуры крайне трудной технической задачей. Неотъемлемой частью верификации микропроцессора является генерация тестовых программ ...
Добавлено: 24 ноября 2017 г.
Татарников А. Д., Камкин А. С., Проценко А. С., Proceedings of the Institute for System Programming of the RAS 2015 Vol. 27 No. 3 P. 125–138
Подсистема памяти является одним из ключевых компонентов микропроцессора. Она включает в себя набор запоминающих устройств различного назначения, объединенных в сложную иерархическую структуру. При этом количество возможных состояний подсистемы крайне велико. По этой причине верификация ее функциональной корректности представляет собой нетривиальную задачу. В настоящее время наиболее часто применяемым на практике подходом к функциональной верификации микропроцессоров является ...
Добавлено: 10 декабря 2017 г.
Создание тестовых программ и анализ результатов их выполнения — основной подход к функциональной верификации микропроцессоров на системном уровне. Имеется множество методов автоматизации разработки тестовых программ, начиная от генерации случайного кода и заканчивая нацеленным построением тестов на основе моделей, однако панацеи не существует: на практике применяются комбинации различных техник, дополняющих друг друга. К сожалению, в настоящее ...
Добавлено: 5 февраля 2018 г.
Татарников А. Д., Камкин А. С., Чупилко М. М. и др., , in: Hardware and Software: Verification and Testing. HVC 2017. Lecture Notes in Computer ScienceVol. 10629: 13th International Haifa Verification Conference, HVC 2017, Haifa, Israel, November 13-15, 2017. Cham: Springer, 2017. P. 217–220.
Добавлено: 24 января 2018 г.
Татарников А. Д., Известия высших учебных заведений. Физика 2016 Т. 59 № 8-2 С. 97–100
В работе предлагается метод автоматизированного построения поведенческих моделей микропроцессоров, используемых при генерации тестовых программ для предсказания результатов их выполнения. Предложенный метод основан на использовании формальных спецификаций системы команд. Данный метод реализован в инструменте MicroTESK, разработанном в ИСП РАН. Инструмент успешно применяется для верификации промышленных микропроцессоров. ...
Добавлено: 2 февраля 2018 г.
Татарников А. Д., , in: Proceedings of IEEE East-West Design & Test Symposium (EWDTS'2016). Yerevan: IEEE, 2016. P. 270–273.
Добавлено: 22 декабря 2017 г.
Татарников А. Д., Камкин А. С., , in: Perspectives of System Informatics - 11th International Andrei P. Ershov Informatics Conference, PSI 2017, Moscow, Russia, June 27-29, 2017, Revised Selected Papers, Lecture Notes in Computer ScienceVol. 10742. Springer, 2018. P. 387–393.
Добавлено: 23 января 2018 г.
Татарников А. Д., Камкин А. С., Сергеева Т. И. и др., , in: Proceedings of the 7th Spring/Summer Young Researchers’ Colloquium on Software Engineering, SYRCoSE 2013. Kazan: -, 2013. P. 51–57 .
Добавлено: 20 декабря 2017 г.
Татарников А. Д., Камкин А. С., Проценко А. С. и др., Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС) 2018 № 2 С. 2–8
В работе рассматривается генератор тестовых программ, предназначенный для верификации микропроцессоров с архитектурой RISC-V. Генератор разработан на основе инструмента MicroTESK и состоит из формальных спецификаций архитектуры RISC-V и архитектурно независимого ядра. Спецификации задают синтаксис и семантику команд. Ядро реализует техники построения последовательностей команд и генерации данных. Генерация осуществляется на основе шаблонов, описывающих структурные и поведенческие свойства программ. Инструмент позволяет расширять ...
Добавлено: 30 октября 2018 г.
Татарников А. Д., Proceedings of the Institute for System Programming of the RAS 2016 Vol. 28 No. 4 P. 77–98
Генерация тестовых программ на языке ассемблера и проверка корректности результатов их выполнения является наиболее широко применяемым подходом к функциональной верификации микропроцессоров. Данная задача решается при помощи специальных автоматизированных средств, называемых генераторами тестовых программ. Высокая сложность современных электронных устройств создает потребность в автоматизированных средствах, способных генерировать тестовые программы, покрывающие нетривиальные ситуации в их работе. Большинство таких ...
Добавлено: 26 ноября 2017 г.
Татарников А. Д., Камкин А. С., Проценко А. С., Известия высших учебных заведений. Физика 2015 Т. 58 № 11-2 С. 70–74
В работе предлагается метод автоматизированного построения тестовых программ, предназначенных для функционального тестирования подсистем памяти одноядерных микропроцессоров. Предложенный метод осно ван на использовании формальных спецификаций механизмов кэширования и трансляции адресов. Различные варианты метода успешно применялись для тестирования промышленных микропроцессоров. ...
Добавлено: 25 января 2018 г.
Татарников А. Д., Камкин А. С., Чупилко М. М. и др., Труды Института системного программирования РАН 2014 Т. 26 № 1 С. 149–200
Обеспечение корректности микропроцессоров и другой микроэлектронной аппаратуры является фундаментальной проблемой, для решения которой применяют разнообразные средства функциональной верификации. В отличие от программ, ошибки в которых исправляются сравнительно просто, дефекты в интегральных схемах (конструктивные и производственные) не могут быть устранены. Несмотря на то, что постоянно совершенствуются системы автоматизированного проектирования (САПР), инструменты генерации тестов и методы анализа ...
Добавлено: 11 декабря 2017 г.
Рассматривается подход к определению базовой стратегии верификации системы на кристалле (СНК) с учетом заданных критериев. Под стратегией понимается комплекс процедур тестирования и верификации с помощью программных и технических средств. Показано, что задача выбора стратегии верификации является сложной многокритериальной задачей принятия решения и может быть представлена как последовательность задач выбора стратегии верификации и распределения затрат на ...
Добавлено: 4 февраля 2015 г.
Камкин А. С., Татарников А. Д., Проценко А. С. и др., , in: 2017 18th International Workshop on Microprocessor and SOC Test and Verification (MTV). IEEE, 2017. P. 10–14.
Добавлено: 18 июля 2018 г.
Карданова Е. Ю., Иванова А. Е., Тарасова К. В. и др., / Series cs.CL "Computation and Language (cs.CL); Artificial Intelligence (cs.AI)". 2024.
The era of large language models (LLM) raises questions not only about how to train models, but also about how to evaluate them. Despite numerous existing benchmarks, insufficient attention is often given to creating assessments that test LLMs in a valid and reliable manner. To address this challenge, we accommodate the Evidence-centered design (ECD) methodology ...
Добавлено: 5 ноября 2024 г.
Камкин А. С., Татарников А. Д., Смолов С. А. и др., , in: 2015 16th International Workshop on Microprocessor and SOC Test and Verification (MTV). IEEE, 2015. P. 1–6.
Добавлено: 18 июля 2018 г.
Татарников А. Д., В кн.: Научно-техническая конференция студентов, аспирантов и молодых специалистов НИУ ВШЭ им. Е.В. Арменского. Материалы конференции. М.: МИЭМ НИУ ВШЭ, 2015. С. 53–54.
В докладе рассказывается об инструменте, позволяющем автоматизировать разработку генераторов тестовых программ для микропроцессоров. В основе работы инструмента лежит использование высокоуровневых формальных спецификаций в качестве источника знания об архитектуре тестируемого микропроцессора. Такой подход помогает сократить трудоемкость разработки тестовых программ и повысить качество тестирования. ...
Добавлено: 13 декабря 2017 г.
Humboldt-Universität zu Berlin, 2016.
This volume contains the papers presented at CS&P 2016, the 25th International Workshop on Concurrency, Specification and Programming, held on September 28 - 30, 2016 in Rostock, Germany. Since the early seventies Warsaw University and Humboldt University have alternately organized an annual workshop - since the early nineties known as CS&P. Over time, it has ...
Добавлено: 13 октября 2016 г.
Татарников А. Д., Труды Института системного программирования РАН 2017 Т. 29 № 1 С. 167–194
В работе дается обзор существующих методов и средств генерации тестовых программ для микропроцессоров. Генерация тестовых программ и анализ результатов их выполнения являются основным подходом к функциональной верификации микропроцессоров. Этот подход также принято называть тестированием. Несмотря на то, что методы генерации тестовых программ непрерывно совершенствуются, тестирование остается крайне трудоемким процессом. Одна из основных причин состоит в ...
Добавлено: 8 ноября 2017 г.
Elena Zamyatina, Alexander Mikov, Roman Mikheev, International Journal "Information Models and Analyses" 2013 Vol. 2 No. 1 P. 70–80
Добавлено: 28 февраля 2015 г.
Smeliansky R. L., Chemeritsky E. V., Захаров В. А., Automatic Control and Computer Sciences 2014 Vol. 48 No. 7 P. 398–406
Добавлено: 30 сентября 2015 г.
Yaroslavl: Yaroslavl State University, 2013.
Workshop on Program Semantics, Specifi cation and Verifi cation: Theory and Applications is the leading event in Russia in the fi eld of applying of the formal methods to software analysis. Proceedings of the fourth workshop are dedicated to formalisms for program semantics, formal models and veri cation, programming and speci fication languages, etc. ...
Добавлено: 14 июля 2013 г.
Филиппов В. А., Хатько Е. Е., Software Engineering 2012 Vol. 2 No. 4 P. 174–179
Проанализированы существующие подходы и алгоритмы для генерации тестов. Предложена аналитическая модель генерации тестов на основе прототипов, учитывающая специфику мобильных приложений. Предложена схема аналитической модели генерации. Представлены численные показатели эффективности предложенной модели. ...
Добавлено: 18 января 2013 г.