?
Specification-Based Test Program Generation for ARM VMSAv8-64 Memory Management Units
P. 1–6.
Татарников А. Д., Камкин А. С., Проценко А. С. и др., Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС) 2018 № 2 С. 2–8
В работе рассматривается генератор тестовых программ, предназначенный для верификации микропроцессоров с архитектурой RISC-V. Генератор разработан на основе инструмента MicroTESK и состоит из формальных спецификаций архитектуры RISC-V и архитектурно независимого ядра. Спецификации задают синтаксис и семантику команд. Ядро реализует техники построения последовательностей команд и генерации данных. Генерация осуществляется на основе шаблонов, описывающих структурные и поведенческие свойства программ. Инструмент позволяет расширять ...
Добавлено: 30 октября 2018 г.
Татарников А. Д., Камкин А. С., Сергеева Т. И. и др., , in: Proceedings of the 7th Spring/Summer Young Researchers’ Colloquium on Software Engineering, SYRCoSE 2013.: Kazan: -, 2013. P. 51–57 .
Добавлено: 20 декабря 2017 г.
Татарников А. Д., Камкин А. С., Чупилко М. М. и др., , 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 Т. II С. 38–45
Генерация тестовых программ и анализ результатов их симуляции на проектной модели являются основным подходом к функциональной верификации микропроцессоров. Верификация – крайне трудоемкий процесс. По некоторым оценкам затраты на нее составляют около 70% от общих трудозатрат на разработку микропроцессора. Это связано с тем, что логика работы современных микропроцессоров содержит огромное количество состояний, и для того, чтобы ...
Добавлено: 12 декабря 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 IEEE East-West Design & Test Symposium (EWDTS'2016).: Yerevan: IEEE, 2016. P. 270–273.
Добавлено: 22 декабря 2017 г.
Татарников А. Д., Камкин А. С., Проценко А. С. и др., Труды Института системного программирования РАН 2016 Т. 28 № 6 С. 87–102
ARM — это семейство микропроцессорных архитектур, разработанных в одноименной компании. Новейшая архитектура этого семейства, ARMv8, содержит большое число команд разных типов и отличается сложной организацией виртуальной памяти (включающей аппаратную поддержку многоуровневой трансляции адресов и виртуализации); все это делает функциональную верификацию микропроцессоров этой архитектуры крайне трудной технической задачей. Неотъемлемой частью верификации микропроцессора является генерация тестовых программ ...
Добавлено: 24 ноября 2017 г.
Камкин А. С., Татарников А. Д., Проценко А. С. и др., , in: 2017 18th International Workshop on Microprocessor and SOC Test and Verification (MTV).: IEEE, 2017. P. 10–14.
Добавлено: 18 июля 2018 г.
Создание тестовых программ и анализ результатов их выполнения — основной подход к функциональной верификации микропроцессоров на системном уровне. Имеется множество методов автоматизации разработки тестовых программ, начиная от генерации случайного кода и заканчивая нацеленным построением тестов на основе моделей, однако панацеи не существует: на практике применяются комбинации различных техник, дополняющих друг друга. К сожалению, в настоящее ...
Добавлено: 5 февраля 2018 г.
Татарников А. Д., Камкин А. С., Проценко А. С., Proceedings of the Institute for System Programming of the RAS 2015 Vol. 27 No. 3 P. 125–138
Подсистема памяти является одним из ключевых компонентов микропроцессора. Она включает в себя набор запоминающих устройств различного назначения, объединенных в сложную иерархическую структуру. При этом количество возможных состояний подсистемы крайне велико. По этой причине верификация ее функциональной корректности представляет собой нетривиальную задачу. В настоящее время наиболее часто применяемым на практике подходом к функциональной верификации микропроцессоров является ...
Добавлено: 10 декабря 2017 г.
Татарников А. Д., Камкин А. С., Проценко А. С., Известия высших учебных заведений. Физика 2015 Т. 58 № 11-2 С. 70–74
В работе предлагается метод автоматизированного построения тестовых программ, предназначенных для функционального тестирования подсистем памяти одноядерных микропроцессоров. Предложенный метод осно ван на использовании формальных спецификаций механизмов кэширования и трансляции адресов. Различные варианты метода успешно применялись для тестирования промышленных микропроцессоров. ...
Добавлено: 25 января 2018 г.
Татарников А. Д., Известия высших учебных заведений. Физика 2016 Т. 59 № 8-2 С. 97–100
В работе предлагается метод автоматизированного построения поведенческих моделей микропроцессоров, используемых при генерации тестовых программ для предсказания результатов их выполнения. Предложенный метод основан на использовании формальных спецификаций системы команд. Данный метод реализован в инструменте MicroTESK, разработанном в ИСП РАН. Инструмент успешно применяется для верификации промышленных микропроцессоров. ...
Добавлено: 2 февраля 2018 г.
Татарников А. Д., Proceedings of the Institute for System Programming of the RAS 2016 Vol. 28 No. 4 P. 77–98
Генерация тестовых программ на языке ассемблера и проверка корректности результатов их выполнения является наиболее широко применяемым подходом к функциональной верификации микропроцессоров. Данная задача решается при помощи специальных автоматизированных средств, называемых генераторами тестовых программ. Высокая сложность современных электронных устройств создает потребность в автоматизированных средствах, способных генерировать тестовые программы, покрывающие нетривиальные ситуации в их работе. Большинство таких ...
Добавлено: 26 ноября 2017 г.
Татарников А. Д., Камкин А. С., , in: Proceedings of the 6th Spring/Summer Young Researchers’ Colloquium on Software Engineering, SYRCoSE 2012.: Perm: -, 2012. P. 64–69.
Добавлено: 13 декабря 2017 г.
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 г.
University of Rzeszow, 2015.
Добавлено: 11 октября 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 г.
Захаров В. А., Подымов В. В., Алтухов В. С. и др., , in: Proceedings of 2014 International Science and Technology Conference "Modern Networking Technologies (MoNeTec): SDN&NFV Next Generation of Computational Infrastructure", Moscow, Russia, October 27-29, 2014.: M.: Max press, 2014. P. 7–12.
Добавлено: 13 октября 2015 г.
Berlin: Humboldt University of Berlin, 2014.
This volume contains the papers presented at CS&P 2014: 23th International Workshop on Concurrency, Specification and Programming held on September 28 - October 1, 2014 in Chemnitz. Since the early seventies Warsaw University and Humboldt-University have alternately organized an annual workshop - since 1993 as CS&P. Over time, it has grown from a bilateral seminar ...
Добавлено: 24 октября 2014 г.
Никольский В. П., Стегайлов В. В., Вычислительные методы и программирование 2015 Т. 16 С. 578–585
Суперкомпьютерные вычисления экзафлопсной эры будут неизбежно ограничены энергоэффективностью. Сегодня в качестве возможных кандидатов для этих целей рассматриваются различные микропроцессорные архитектуры. Недавно микропроцессоры с архитектурой ARM в своем развитии достигли момента, когда уже можно серьезно обсуждать их применение для высокопроизводительных вычислений. В настоящей статье представлен анализ эффективности последних версий ARM-микропроцессоров и их производительности для задач классической ...
Добавлено: 16 ноября 2015 г.
Кудряшов Е. А., Мельник Д. М., Монаков А. В., Труды Института системного программирования РАН 2016 Т. 28 № 1 С. 63–80
В статье рассматривается подход к оптимизации вызовов внешних функций в позиционно-независимом коде, основанный на выдаче вызовов непосредственно через глобальную таблицу смещений (GOT), минуя таблицу компоновки процедур (PLT). Стандартные механизмы кодогенерации на операционной системе Linux предполагают создание PLT не только для основного модуля (который является позиционно-зависимым и полагается на механизм PLT для вызовов внешних процедур), но ...
Добавлено: 5 ноября 2018 г.