?
Построение поведенческих моделей микропроцессоров для генерации тестовых программ
Известия высших учебных заведений. Физика. 2016. Т. 59. № 8-2 . С. 97-100.
В работе предлагается метод автоматизированного построения поведенческих моделей микропроцессоров, используемых при генерации тестовых программ для предсказания результатов их выполнения. Предложенный метод основан на использовании формальных спецификаций системы команд. Данный метод реализован в инструменте MicroTESK, разработанном в ИСП РАН. Инструмент успешно применяется для верификации промыш-
ленных микропроцессоров.
Научное направление:
Компьютерные науки
Приоритетные направления:
компьютерно-математическое
Язык:
русский
Татарников А. Д., Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС) 2016 Т. II С. 38-45
Генерация тестовых программ и анализ результатов их симуляции на проектной модели являются основным подходом к функциональной верификации микропроцессоров. Верификация – крайне трудоемкий процесс. По некоторым оценкам затраты на нее составляют около 70% от общих трудозатрат на разработку микропроцессора. Это связано с тем, что логика работы современных микропроцессоров содержит огромное количество состояний, и для того, чтобы ...
Добавлено: 12 декабря 2017 г.
Татарников А. Д., Камкин А. С., Проценко А. С., Proceedings of the Institute for System Programming of the RAS 2015 Vol. 27 No. 3 P. 125-138
Подсистема памяти является одним из ключевых компонентов микропроцессора. Она включает в себя набор запоминающих устройств различного назначения, объединенных в сложную иерархическую структуру. При этом количество возможных состояний подсистемы крайне велико. По этой причине верификация ее функциональной корректности представляет собой нетривиальную задачу. В настоящее время наиболее часто применяемым на практике подходом к функциональной верификации микропроцессоров является ...
Добавлено: 10 декабря 2017 г.
Татарников А. Д., Камкин А. С., Проценко А. С. и др., Труды Института системного программирования РАН 2016 Т. 28 № 6 С. 87-102
ARM — это семейство микропроцессорных архитектур, разработанных в одноименной компании. Новейшая архитектура этого семейства, ARMv8, содержит большое число команд разных типов и отличается сложной организацией виртуальной памяти (включающей аппаратную поддержку многоуровневой трансляции адресов и виртуализации); все это делает функциональную верификацию микропроцессоров этой архитектуры крайне трудной технической задачей. Неотъемлемой частью верификации микропроцессора является генерация тестовых программ ...
Добавлено: 24 ноября 2017 г.
Татарников А. Д., Камкин А. С., Проценко А. С. и др., Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС) 2018 № 2 С. 2-8
В работе рассматривается генератор тестовых программ, предназначенный для верификации микропроцессоров с архитектурой RISC-V. Генератор разработан на основе инструмента MicroTESK и состоит из формальных спецификаций архитектуры RISC-V и архитектурно независимого ядра. Спецификации задают синтаксис и семантику команд. Ядро реализует техники построения последовательностей команд и генерации данных. Генерация осуществляется на основе шаблонов, описывающих структурные и поведенческие свойства программ. Инструмент позволяет расширять ...
Добавлено: 30 октября 2018 г.
Создание тестовых программ и анализ результатов их выполнения — основной подход к функциональной верификации микропроцессоров на системном уровне. Имеется множество методов автоматизации разработки тестовых программ, начиная от генерации случайного кода и заканчивая нацеленным построением тестов на основе моделей, однако панацеи не существует: на практике применяются комбинации различных техник, дополняющих друг друга. К сожалению, в настоящее ...
Добавлено: 5 февраля 2018 г.
Татарников А. Д., , in : Proceedings of IEEE East-West Design & Test Symposium (EWDTS'2016). : Yerevan : IEEE, 2016. P. 270-273.
Добавлено: 22 декабря 2017 г.
Татарников А. Д., Камкин А. С., Проценко А. С., Известия высших учебных заведений. Физика 2015 Т. 58 № 11-2 С. 70-74
В работе предлагается метод автоматизированного построения тестовых программ, предназначенных для функционального тестирования подсистем памяти одноядерных микропроцессоров. Предложенный метод осно ван на использовании формальных спецификаций механизмов кэширования и трансляции адресов. Различные варианты метода успешно применялись для тестирования промышленных микропроцессоров. ...
Добавлено: 25 января 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 г.
Татарников А. Д., Камкин А. С., Сергеева Т. И. и др., , 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 Science. Vol. 10629: 13th International Haifa Verification Conference, HVC 2017, Haifa, Israel, November 13-15, 2017.: Cham : Springer, 2017. P. 217-220.
Добавлено: 24 января 2018 г.
Татарников А. Д., Proceedings of the Institute for System Programming of the RAS 2016 Vol. 28 No. 4 P. 77-98
Генерация тестовых программ на языке ассемблера и проверка корректности результатов их выполнения является наиболее широко применяемым подходом к функциональной верификации микропроцессоров. Данная задача решается при помощи специальных автоматизированных средств, называемых генераторами тестовых программ. Высокая сложность современных электронных устройств создает потребность в автоматизированных средствах, способных генерировать тестовые программы, покрывающие нетривиальные ситуации в их работе. Большинство таких ...
Добавлено: 26 ноября 2017 г.
Татарников А. Д., Камкин А. С., Чупилко М. М. и др., Труды Института системного программирования РАН 2014 Т. 26 № 1 С. 149-200
Обеспечение корректности микропроцессоров и другой микроэлектронной аппаратуры является фундаментальной проблемой, для решения которой применяют разнообразные средства функциональной верификации. В отличие от программ, ошибки в которых исправляются сравнительно просто, дефекты в интегральных схемах (конструктивные и производственные) не могут быть устранены. Несмотря на то, что постоянно совершенствуются системы автоматизированного проектирования (САПР), инструменты генерации тестов и методы анализа ...
Добавлено: 11 декабря 2017 г.
Vladimir A. Bashkin, Irina A. Lomazova, Transactions on Petri Nets and Other Models of Concurrency 2014 Vol. 9 P. 1-18
A resource workflow net (RWF-net) is a workflow net, supplied with an additional set of initially marked resource places. Resources can be consumed and/or produced by transitions. Neither the intermediate nor final resource markings are constrained, hence a net can have an infinite number of different reachable states. An RWF-net with k tokens in the ...
Добавлено: 7 декабря 2014 г.
Жигалова М. А., Сухов А. О., Известия Южного федерального университета. Технические науки 2015 № 2 С. 126-134
В процессе разработки и сопровождения программных продуктов создается и используется большое число проектных документов. Для автоматизации их обработки и контроля упомянутых в документах требований к разрабатываемому продукту требуется создание инструментальных средств поддержки работы аналитика при проектировании информационных систем. Для того чтобы существовала возможность выполнять контроль каждого вида требований в отдельности необходимо выделить в проектном документе ...
Добавлено: 12 декабря 2014 г.
Внуков А. А., Шабном М., Вестник Российского университета дружбы народов. Серия: Инженерные исследования 2014 № 3 С. 38-46
В статье рассматриваются математические модели задач кинематики прямой, обратной, позиционирования захвата робота. Программные реализации этих задач позволили провести исследования сходимости и точности решений обратной задачи в зависимости от начальных значений, диапазона значений углов на каждой итерации и получить графики зависимостей точности от итераций и уменьшения углов. Для уточнения решения обратной задачи кинематики применяется результат решения ...
Добавлено: 26 июля 2014 г.
В.А. Башкин, И.А. Ломазова, Cybernetics and Systems Analysis 2011 № 2 С. 31-39
Рассматривается проблема моделирования мультиагентных систем с бесконечным множеством состояний. Исследуются формализмы, основанные на обобщении сетей активных ресурсов. Определены новые способы моделирования: параметризованные АР-сети, двухуровневые АР-схемы и двухуровневые АР-сети. Показано, что эти формализмы обладают удобным синтаксисом для моделирования мультиагентных систем, в том числе систем со сложной модульной или иерархической структурой. Доказано, что параметризованные АР-сети и двухуровневые ...
Добавлено: 19 марта 2011 г.
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 г.
Описываются средства DSM-платформы MetaLanguage для создания предметно-ориентированных языков и многоуровневого моделирования. Возможность определения трансформаций обеспечивает снижение трудоёмкости разработки новых языков и преобразования моделей. ...
Добавлено: 17 ноября 2013 г.
Вишнеков А. В., Иванова Е. М., Басова К. Э. и др., Информационные технологии 2019 Т. 25 № 8 С. 490-501
Рассматриваются вопросы моделирования работы функциональных блоков вычислительной системы, требования к моделям с точки зрения решения образовательных и исследовательских задач. Предлагается структура моделирующего комплекса, способы визуализации компонентов архитектуры и принципов функционирования блоков вычислительной системы. Приводятся описания алгоритмов работы моделирующих программ. ...
Добавлено: 29 августа 2019 г.
Tsareva O. O., Zelenyi L. M., Malova H. V. и др., Physics-Uspekhi 2018 Vol. 61 No. 2 P. 191-202
Добавлено: 8 мая 2018 г.
Разработана компьютерная программа, предназначенная для прогнозирования результатов чемпионата мира 2013 года по легкой атлетике на дистанции 100 метров у мужчин. В основе программы лежит нейронная сеть, обученная на результатах предыдущих чемпионатов мира. Имеется демонстрационный прототип, который оценивает шансы на победу для каждого из пяти возможных претендентов. Помимо прогнозов программа позволяет оценивать влияние изменения параметров, характеризующих ...
Добавлено: 6 декабря 2012 г.
Cardiff : IEEE Computer Society, 2013
Добавлено: 13 марта 2015 г.
Ясницкий Л. Н., Dumler A. A., Bogdanov K. и др., Biomedical Engineering 2013 Vol. 47 No. 3 P. 160-163
Создана нейро-экспертная система диагностики и прогнозирования развития сердечно-сосудистых заболеваний. С помощью разработанной системы выявлены неизвестные ранее медицинские знания, которые предлагается учитывать при разработке рекомендаций профилактики и лечения кардиологических больных. ...
Добавлено: 19 ноября 2013 г.