?
Генерация тестовых программ для микропроцессоров на основе спецификаций подсистем памяти
Известия высших учебных заведений. Физика. 2015. Т. 58. № 11-2. С. 70-74.
В работе предлагается метод автоматизированного построения тестовых программ, предназначенных для функционального тестирования подсистем памяти одноядерных микропроцессоров. Предложенный метод осно-
ван на использовании формальных спецификаций механизмов кэширования и трансляции адресов. Различные варианты метода успешно применялись для тестирования промышленных микропроцессоров.
Татарников А. Д., Камкин А. С., Проценко А. С., Proceedings of the Institute for System Programming of the RAS 2015 Vol. 27 No. 3 P. 125-138
Подсистема памяти является одним из ключевых компонентов микропроцессора. Она включает в себя набор запоминающих устройств различного назначения, объединенных в сложную иерархическую структуру. При этом количество возможных состояний подсистемы крайне велико. По этой причине верификация ее функциональной корректности представляет собой нетривиальную задачу. В настоящее время наиболее часто применяемым на практике подходом к функциональной верификации микропроцессоров является ...
Добавлено: 10 декабря 2017 г.
Татарников А. Д., Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС) 2016 Т. II С. 38-45
Генерация тестовых программ и анализ результатов их симуляции на проектной модели являются основным подходом к функциональной верификации микропроцессоров. Верификация – крайне трудоемкий процесс. По некоторым оценкам затраты на нее составляют около 70% от общих трудозатрат на разработку микропроцессора. Это связано с тем, что логика работы современных микропроцессоров содержит огромное количество состояний, и для того, чтобы ...
Добавлено: 12 декабря 2017 г.
Татарников А. Д., Известия высших учебных заведений. Физика 2016 Т. 59 № 8-2 С. 97-100
В работе предлагается метод автоматизированного построения поведенческих моделей микропроцессоров, используемых при генерации тестовых программ для предсказания результатов их выполнения. Предложенный метод основан на использовании формальных спецификаций системы команд. Данный метод реализован в инструменте MicroTESK, разработанном в ИСП РАН. Инструмент успешно применяется для верификации промышленных микропроцессоров. ...
Добавлено: 2 февраля 2018 г.
Татарников А. Д., Камкин А. С., , 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 г.
Татарников А. Д., Камкин А. С., Проценко А. С. и др., Труды Института системного программирования РАН 2016 Т. 28 № 6 С. 87-102
ARM — это семейство микропроцессорных архитектур, разработанных в одноименной компании. Новейшая архитектура этого семейства, ARMv8, содержит большое число команд разных типов и отличается сложной организацией виртуальной памяти (включающей аппаратную поддержку многоуровневой трансляции адресов и виртуализации); все это делает функциональную верификацию микропроцессоров этой архитектуры крайне трудной технической задачей. Неотъемлемой частью верификации микропроцессора является генерация тестовых программ ...
Добавлено: 24 ноября 2017 г.
Татарников А. Д., Камкин А. С., Проценко А. С. и др., Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС) 2018 № 2 С. 2-8
В работе рассматривается генератор тестовых программ, предназначенный для верификации микропроцессоров с архитектурой RISC-V. Генератор разработан на основе инструмента MicroTESK и состоит из формальных спецификаций архитектуры RISC-V и архитектурно независимого ядра. Спецификации задают синтаксис и семантику команд. Ядро реализует техники построения последовательностей команд и генерации данных. Генерация осуществляется на основе шаблонов, описывающих структурные и поведенческие свойства программ. Инструмент позволяет расширять ...
Добавлено: 30 октября 2018 г.
Татарников А. Д., Камкин А. С., Чупилко М. М. и др., , 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 г.
Татарников А. Д., , in : Proceedings of IEEE East-West Design & Test Symposium (EWDTS'2016). : Yerevan : IEEE, 2016. P. 270-273.
Добавлено: 22 декабря 2017 г.
Создание тестовых программ и анализ результатов их выполнения — основной подход к функциональной верификации микропроцессоров на системном уровне. Имеется множество методов автоматизации разработки тестовых программ, начиная от генерации случайного кода и заканчивая нацеленным построением тестов на основе моделей, однако панацеи не существует: на практике применяются комбинации различных техник, дополняющих друг друга. К сожалению, в настоящее ...
Добавлено: 5 февраля 2018 г.
Татарников А. Д., 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 г.
Камкин А. С., Татарников А. Д., Смолов С. А. и др., , in : 2015 16th International Workshop on Microprocessor and SOC Test and Verification (MTV). : IEEE, 2015. P. 1-6.
Добавлено: 18 июля 2018 г.
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 г.
Татарников А. Д., Камкин А. С., Чупилко М. М. и др., Труды Института системного программирования РАН 2014 Т. 26 № 1 С. 149-200
Обеспечение корректности микропроцессоров и другой микроэлектронной аппаратуры является фундаментальной проблемой, для решения которой применяют разнообразные средства функциональной верификации. В отличие от программ, ошибки в которых исправляются сравнительно просто, дефекты в интегральных схемах (конструктивные и производственные) не могут быть устранены. Несмотря на то, что постоянно совершенствуются системы автоматизированного проектирования (САПР), инструменты генерации тестов и методы анализа ...
Добавлено: 11 декабря 2017 г.
Yaroslavl : Ярославский государственный университет им. П.Г. Демидова, 2018
Добавлено: 26 октября 2018 г.
Дворянский Л. В., Фрумин Д. И., , in : Proceedings of the 6th Spring/Summer Young Researchers’ Colloquium on Software Engineering, SYRCoSE 2012. : Perm : -, 2012. P. 122-127.
Nested Petri nets is an extension of Petri net formalism with net tokens for modelling multi-agent distributed systems with complex structure. Temporal logics, such as CTL, are used to state requirements of software systems behaviour. However, in the case of nested Petri nets models, CTL is not expressive enough for specification of system behaviour. In ...
Добавлено: 20 сентября 2012 г.
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, 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 г.
Татарников А. Д., В кн. : Научно-техническая конференция студентов, аспирантов и молодых специалистов НИУ ВШЭ им. Е.В. Арменского. Материалы конференции. : М. : МИЭМ НИУ ВШЭ, 2015. С. 53-54.
В докладе рассказывается об инструменте, позволяющем автоматизировать разработку генераторов тестовых программ для микропроцессоров. В основе работы инструмента лежит использование высокоуровневых формальных спецификаций в качестве источника знания об архитектуре тестируемого микропроцессора. Такой подход помогает сократить трудоемкость разработки тестовых программ и повысить качество тестирования. ...
Добавлено: 13 декабря 2017 г.
Якименко С. И., В кн. : Современные сетевые технологии: труды 4-й Международной конференции "Современные сетевые технологии" (MoNeTec-2022), 27-29 октября 2022 г., г.Москва (короткие и стендовые доклады). : М. : Издательский отдел факультета ВМК МГУ им. М.В. Ломоносова, 2022. С. 70-76.
Статья посвящена вопросам кэширования в информационно-ориентированных сетях (information-centric networks, ICN), направленных на адресацию по имени контента и отделение информации от её узла-производителя. Внутрисетевое кэширование является одной из главных особенностей ICN, превращая их, по сути, в сеть взаимосвязанных кэшей, способных накапливать пакеты в буфере промежуточных маршрутизаторов, а также приближать их к потребителю с помощью периферийного кэша. ...
Добавлено: 20 декабря 2022 г.
Bialystok : Bialystok University of Technology, 2013
This volume contains the Proceedings of 22nd Concurrency, Specification and Programming (GS&P) Workshop held on September 25-27, 2013 in Warsaw. There were 48 submissions. Each submission was reviewed by two program committee members. The committee decided to accept 40 papers. The Workshop was initiated in the mid 1970s by computer scientists and mathematicians from Warsaw ...
Добавлено: 30 сентября 2013 г.
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 г.