?
Генератор тестовых программ для архитектуры RISC-V на основе инструмента MicroTESK
Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС). 2018. № 2. С. 2-8.
В работе рассматривается генератор тестовых программ, предназначенный для верификации микропроцессоров с архитектурой RISC-V. Генератор разработан на основе инструмента MicroTESK и состоит из формальных спецификаций архитектуры RISC-V и архитектурно независимого ядра. Спецификации задают синтаксис и семантику команд. Ядро реализует техники построения последовательностей команд и генерации данных. Генерация осуществляется на основе шаблонов, описывающих структурные и поведенческие свойства программ. Инструмент позволяет расширять систему команд и поддерживает случайные, комбинаторные и основанные на ограничениях техники генерации.
Научное направление:
Компьютерные науки
Приоритетные направления:
компьютерно-математическое
Язык:
русский
Татарников А. Д., Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС) 2016 Т. II С. 38-45
Генерация тестовых программ и анализ результатов их симуляции на проектной модели являются основным подходом к функциональной верификации микропроцессоров. Верификация – крайне трудоемкий процесс. По некоторым оценкам затраты на нее составляют около 70% от общих трудозатрат на разработку микропроцессора. Это связано с тем, что логика работы современных микропроцессоров содержит огромное количество состояний, и для того, чтобы ...
Добавлено: 12 декабря 2017 г.
Татарников А. Д., Камкин А. С., Проценко А. С. и др., Труды Института системного программирования РАН 2016 Т. 28 № 6 С. 87-102
ARM — это семейство микропроцессорных архитектур, разработанных в одноименной компании. Новейшая архитектура этого семейства, ARMv8, содержит большое число команд разных типов и отличается сложной организацией виртуальной памяти (включающей аппаратную поддержку многоуровневой трансляции адресов и виртуализации); все это делает функциональную верификацию микропроцессоров этой архитектуры крайне трудной технической задачей. Неотъемлемой частью верификации микропроцессора является генерация тестовых программ ...
Добавлено: 24 ноября 2017 г.
Татарников А. Д., Известия высших учебных заведений. Физика 2016 Т. 59 № 8-2 С. 97-100
В работе предлагается метод автоматизированного построения поведенческих моделей микропроцессоров, используемых при генерации тестовых программ для предсказания результатов их выполнения. Предложенный метод основан на использовании формальных спецификаций системы команд. Данный метод реализован в инструменте MicroTESK, разработанном в ИСП РАН. Инструмент успешно применяется для верификации промышленных микропроцессоров. ...
Добавлено: 2 февраля 2018 г.
Создание тестовых программ и анализ результатов их выполнения — основной подход к функциональной верификации микропроцессоров на системном уровне. Имеется множество методов автоматизации разработки тестовых программ, начиная от генерации случайного кода и заканчивая нацеленным построением тестов на основе моделей, однако панацеи не существует: на практике применяются комбинации различных техник, дополняющих друг друга. К сожалению, в настоящее ...
Добавлено: 5 февраля 2018 г.
Татарников А. Д., Камкин А. С., Проценко А. С., Proceedings of the Institute for System Programming of the RAS 2015 Vol. 27 No. 3 P. 125-138
Подсистема памяти является одним из ключевых компонентов микропроцессора. Она включает в себя набор запоминающих устройств различного назначения, объединенных в сложную иерархическую структуру. При этом количество возможных состояний подсистемы крайне велико. По этой причине верификация ее функциональной корректности представляет собой нетривиальную задачу. В настоящее время наиболее часто применяемым на практике подходом к функциональной верификации микропроцессоров является ...
Добавлено: 10 декабря 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 Science. Vol. 10742.: Springer, 2018. P. 387-393.
Добавлено: 23 января 2018 г.
Татарников А. Д., , in : Proceedings of IEEE East-West Design & Test Symposium (EWDTS'2016). : Yerevan : IEEE, 2016. P. 270-273.
Добавлено: 22 декабря 2017 г.
Татарников А. Д., Камкин А. С., Чупилко М. М. и др., , in : Hardware and Software: Verification and Testing. HVC 2017. Lecture Notes in Computer Science. Vol. 10629: 13th International Haifa Verification Conference, HVC 2017, Haifa, Israel, November 13-15, 2017.: Cham : Springer, 2017. P. 217-220.
Добавлено: 24 января 2018 г.
Татарников А. Д., Камкин А. С., Сергеева Т. И. и др., , in : Proceedings of the 7th Spring/Summer Young Researchers’ Colloquium on Software Engineering, SYRCoSE 2013. : Kazan : -, 2013. P. 51-57 .
Добавлено: 20 декабря 2017 г.
Татарников А. Д., Proceedings of the Institute for System Programming of the RAS 2016 Vol. 28 No. 4 P. 77-98
Генерация тестовых программ на языке ассемблера и проверка корректности результатов их выполнения является наиболее широко применяемым подходом к функциональной верификации микропроцессоров. Данная задача решается при помощи специальных автоматизированных средств, называемых генераторами тестовых программ. Высокая сложность современных электронных устройств создает потребность в автоматизированных средствах, способных генерировать тестовые программы, покрывающие нетривиальные ситуации в их работе. Большинство таких ...
Добавлено: 26 ноября 2017 г.
Камкин А. С., Татарников А. Д., Проценко А. С. и др., , in : 2017 18th International Workshop on Microprocessor and SOC Test and Verification (MTV). : IEEE, 2017. P. 10-14.
Добавлено: 18 июля 2018 г.
Yaroslavl : Ярославский государственный университет им. П.Г. Демидова, 2018
Добавлено: 26 октября 2018 г.
Татарников А. Д., Камкин А. С., Проценко А. С., Известия высших учебных заведений. Физика 2015 Т. 58 № 11-2 С. 70-74
В работе предлагается метод автоматизированного построения тестовых программ, предназначенных для функционального тестирования подсистем памяти одноядерных микропроцессоров. Предложенный метод осно ван на использовании формальных спецификаций механизмов кэширования и трансляции адресов. Различные варианты метода успешно применялись для тестирования промышленных микропроцессоров. ...
Добавлено: 25 января 2018 г.
Татарников А. Д., Камкин А. С., Чупилко М. М. и др., Труды Института системного программирования РАН 2014 Т. 26 № 1 С. 149-200
Обеспечение корректности микропроцессоров и другой микроэлектронной аппаратуры является фундаментальной проблемой, для решения которой применяют разнообразные средства функциональной верификации. В отличие от программ, ошибки в которых исправляются сравнительно просто, дефекты в интегральных схемах (конструктивные и производственные) не могут быть устранены. Несмотря на то, что постоянно совершенствуются системы автоматизированного проектирования (САПР), инструменты генерации тестов и методы анализа ...
Добавлено: 11 декабря 2017 г.
Zakharov V.A., Volkanov D. Y., Zorin D. A. и др., Programming and Computer Software 2015 Vol. 41 No. 6 P. 325-335
Checking the correctness of distributed systems is one of the most difficult and urgent problems in software engineering. A combined toolset for the verification of real-time distributed systems (RTDS) is described. RTDSs are specified as statecharts in the Universal Modeling Language (UML). The semantics of statecharts is defined by means of hierarchical timed automata. The ...
Добавлено: 13 октября 2015 г.
Камкин А. С., Чупилко М. М., Смолов С. А. и др., , in : 2018 19th International Workshop on Microprocessor and SOC Test and Verification (MTV). : Austin : IEEE Computer Society, 2018. P. 6-11.
Добавлено: 3 июля 2019 г.
Камкин А. С., М. : МАКС Пресс, 2018
Книга является учебным пособием по формальным методам верификации программ и основана на курсах лекций, читаемых автором на факультете ВМК МГУ имени М.В. Ломоносова, ФУПМ МФТИ и ФКН ВШЭ. В ней изложены основы таких подходов, как дедуктивный анализ и проверка моделей. Список тем включает: методы формализации семантики языков программирования (операционная и аксиоматическая семантика), методы формальной спецификации ...
Добавлено: 2 ноября 2018 г.
Захаров В. А., Волканов Д. Ю., Зорин Д. А. и др., Программирование 2015 № 6 С. 72-86
Проверка правильности функционирования распределенных программ --- это одна из наиболее трудных и актуальных задач современного программирования. В статье описано комбинированное программно-инструментальное средство верификации распределенных вычислительных систем реального времени (РВС РВ). Для описания РВС РВ используется универсальный язык моделирования UML. Семантика диаграмм состояний UML определяется на основе модели вычислений иерархических временных автоматов. Средство верификации диаграмм UML ...
Добавлено: 13 октября 2015 г.
Камкин А. С., Татарников А. Д., Смолов С. А. и др., , in : 2015 16th International Workshop on Microprocessor and SOC Test and Verification (MTV). : IEEE, 2015. P. 1-6.
Добавлено: 18 июля 2018 г.
Smeliansky R. L., Chemeritsky E. V., Захаров В. А., Automatic Control and Computer Sciences 2014 Vol. 48 No. 7 P. 398-406
Добавлено: 30 сентября 2015 г.
Рассматривается подход к определению базовой стратегии верификации системы на кристалле (СНК) с учетом заданных критериев. Под стратегией понимается комплекс процедур тестирования и верификации с помощью программных и технических средств. Показано, что задача выбора стратегии верификации является сложной многокритериальной задачей принятия решения и может быть представлена как последовательность задач выбора стратегии верификации и распределения затрат на ...
Добавлено: 4 февраля 2015 г.
В.А. Башкин, И.А. Ломазова, Cybernetics and Systems Analysis 2011 № 2 С. 31-39
Рассматривается проблема моделирования мультиагентных систем с бесконечным множеством состояний. Исследуются формализмы, основанные на обобщении сетей активных ресурсов. Определены новые способы моделирования: параметризованные АР-сети, двухуровневые АР-схемы и двухуровневые АР-сети. Показано, что эти формализмы обладают удобным синтаксисом для моделирования мультиагентных систем, в том числе систем со сложной модульной или иерархической структурой. Доказано, что параметризованные АР-сети и двухуровневые ...
Добавлено: 19 марта 2011 г.
Yaroslavl : Yaroslavl State University, 2013
Workshop on Program Semantics, Specification and Verification: Theory and Applications is the leading event in Russia in the field of applying of the formal methods to software analysis. Proceedings of the fourth workshop are dedicated to formalisms for program semantics, formal models and verication, programming and specification languages, etc. ...
Добавлено: 14 июля 2013 г.