• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • A
  • A
  • A
  • A
  • A
Обычная версия сайта
  • RU
  • EN
  • Национальный исследовательский университет «Высшая школа экономики»
  • Публикации ВШЭ
  • Глава
  • Принципы разработки компонента системы SDVRP для проверки свойств безопасности ПО микроконтроллера ARM
  • RU
  • EN
Расширенный поиск
Высшая школа экономики
Национальный исследовательский университет
Приоритетные направления
  • бизнес-информатика
  • государственное и муниципальное управление
  • гуманитарные науки
  • инженерные науки
  • компьютерно-математическое
  • математика
  • менеджмент
  • право
  • социология
  • экономика
по году
  • 2027
  • 2026
  • 2025
  • 2024
  • 2023
  • 2022
  • 2021
  • 2020
  • 2019
  • 2018
  • 2017
  • 2016
  • 2015
  • 2014
  • 2013
  • 2012
  • 2011
  • 2010
  • 2009
  • 2008
  • 2007
  • 2006
  • 2005
  • 2004
  • 2003
  • 2002
  • 2001
  • 2000
  • 1999
  • 1998
  • 1997
  • 1996
  • 1995
  • 1994
  • 1993
  • 1992
  • 1991
  • 1990
  • 1989
  • 1988
  • 1987
  • 1986
  • 1985
  • 1984
  • 1983
  • 1982
  • 1981
  • 1980
  • 1979
  • 1978
  • 1977
  • 1976
  • 1975
  • 1974
  • 1973
  • 1972
  • 1971
  • 1970
  • 1969
  • 1968
  • 1967
  • 1966
  • 1965
  • 1964
  • 1963
  • 1958
  • еще
Тематика
Новости
18 мая 2026 г.
В Вышке прошла XXX юбилейная научно-техническая конференция имени Е.В. Арменского
Организатором научного события выступает Московский институт электроники и математики им. А.Н. Тихонова ВШЭ. В этом году главный инженерный студенческий форум проходил 30-й раз и собрал рекордное число участников. Студенты, аспиранты и молодые специалисты из 50 вузов и организаций России представили научно-исследовательские доклады в ИТ-области. Отдельная секция была посвящена научно-исследовательским работам школьников.
15 мая 2026 г.
В НИУ ВШЭ разрабатывают нейросеть для сферы науки и инноваций
Исследователи НИУ ВШЭ учат большие языковые модели понимать русскоязычную научную терминологию, увеличивая при этом их энергоэффективность. Адаптированная модель работает в 2,7 раза быстрее и требует на 73% меньше памяти, чем исходная открытая модель, что позволяет запускать ее на более доступном оборудовании. Программа прошла государственную регистрацию.
15 мая 2026 г.
Стартовал совместный спецпроект бренд-медиа Вышки IQ Media и iFORA ИСИЭЗ
В мае 2026 года стартовал научно-популярный проект «Искусственный интеллект: технологии, данные и будущее», который стал результатом работы двух команд — проекта iFORA Института статистических исследований и экономики знаний НИУ ВШЭ и редакции бренд-медиа IQMedia. Медийно-аналитический спецпроект посвящен современному развитию искусственного интеллекта и аналитике больших данных.

 

Нашли опечатку?
Выделите её, нажмите Ctrl+Enter и отправьте нам уведомление. Спасибо за участие!

Публикации
  • Книги
  • Статьи
  • Главы в книгах
  • Препринты
  • Верификация публикаций
  • Расширенный поиск
  • Правила использования материалов
  • Наука в ВШЭ

?

Принципы разработки компонента системы SDVRP для проверки свойств безопасности ПО микроконтроллера ARM

С. 112–128.
С. А. Шершаков

Вопрос корректности программного обеспечения является одним из непреходящих в области информационных технологий. Обычно под корректностью программы подразумевают соответствие рассматриваемой программы  некоторой определенным образом заданной спецификации. Обычно спецификация явно определяет, что должна делать эта система, не касаясь вопроса, каким образом. Проблема тестирования и верификации программно-аппаратных комплексов неоднократно поднималась в научных работах. Данная работа посвящена вопросам верификации ПО микроконтроллерной (МК) системы на платформе SDVRP. Целью работы являются методики выявления правил, составляющих модель верификации, и адаптация SDVRP для специфических условий разработки ПО для МК.

Язык: русский
Полный текст
Ключевые слова: верификациятестирование программмикроконтроллерыARMSDVRP

В книге

XIII Апрельская международная научная конференция по проблемам развития экономики и общества: сборник студенческих работ
XIII Апрельская международная научная конференция по проблемам развития экономики и общества: сборник студенческих работ
М.: Издательский дом НИУ ВШЭ, 2014.
Похожие публикации
Сравнение временных характеристик операционных систем реального времени на микроконтроллерах с архитектурами ядер ARM И RISC-V
Махмудов Т. Н., Дубленский Д. С., Канунников Е. И., Машиностроение: сетевой электронный научный журнал 2025 Т. 12 № 4 С. 15–21
Операционные системы реального времени (ОСРВ - RTOS) занимают важное место в современных технологических процессах, становясь неотъемлемой частью множества отраслей и производственных циклов. Эти системы обладают уникальными характеристиками, позволяющими эффективно управлять ресурсами и обеспечивать высокую скорость отклика на внешние события. Такая особенность базируется на способности ОСРВ перераспределять ресурсы между различными задачами с разным приоритетом, гарантируя выполнение ...
Добавлено: 8 мая 2026 г.
Имитационное моделирование. Теория и практика (ИММОД 2025)
СПб.: АО "ЦТСС", 2025.
В научном издании представлены труды Двенадцатой всероссийской научно-практической конференции по имитационному моделированию и его применению в науке и промышленности «Имитационное моделирование. Теория и практика» (ИММОД-2025) по следующим направлениям: - теоретические основы и методология имитационного и комплексного моделирования; - методы исследования и оценки качества моделей, валидация и верификации моделей; - методы и системы распределенного моделирования; - ...
Добавлено: 17 апреля 2026 г.
Evaluation of Correlation Functions and Multi-model Forecasting of Geopotential Height and Temperature in the Troposphere and Lower Stratosphere
Гордин В. А., Smirnov M. A., Russian Meteorology and Hydrology 2025 No. 50 P. 1016–1028
Для интерполяции комплексного прогноза геопотенциала и температуры в точки регулярной сетки проводилась статистическая оценка трехмерных авто- и кросс-кореляционных функций для инкрементов от первого приближения. В качестве первого приближения использованы поля прогноза по модели ICON. ...
Добавлено: 17 февраля 2026 г.
InGrid: Towards a Simulation-Based Automated Decision-Making System for Transportation
Степанянц В. Г., , in: 2025 International Russian Automation Conference (RusAutoCon).: IEEE, 2025. P. 982–986.
Добавлено: 3 октября 2025 г.
Лабораторные работы на базе ESP32
Сомов А. С., Степанов А. С., Лыжин И. Г., М.: Сколковский институт науки и технологий, 2022.
Сомов А.С., Степанов А.С., Лыжин И.Г. Методическое пособие «Лабораторные работы на базе ESP32» / Сомов А.С., Степанов А.С., Лыжин И.Г. – М: Сколковский институт науки и технологий, 2022. – 33 с. УДК 372.862, 004.9 Методическое пособие предназначено для всех, кто интересуется технологией Интернет Вещей (англ. Internet of Things, IoT). В пособии рассмотрена работа с отладочной платой на базе микроконтроллера ESP32 и датчиком ...
Добавлено: 2 октября 2025 г.
Wind Speed Analysis Method within WRF-ARW Tropical Cyclone Modeling
Poplavsky E., Кузнецова А. М., Troitskaya Y., Journal of Marine Science and Engineering 2023 Vol. 11 No. 6 Article 1239
В данной работе представлен анализ нового метода восстановления параметров пограничного слоя атмосферы в ураганах. Данный метод основан на аппроксимации верхней параболической части профиля скорости ветра и восстановлении нижней логарифмической части. На основе логарифмической части получены скорость трения, скорость приземного ветра и коэффициент аэродинамического сопротивления. Полученные данные используются для верификации данных моделирования в модели WRF-ARW. Изучен ...
Добавлено: 10 декабря 2024 г.
О проблеме доказательств в историческом исследовании, или Подозревал ли Петр I патриарха Адриана в связях с мятежными стрельцами?
Акельев Е. В., ВИВЛIОθИКА: E-Journal of Eighteenth-Century Russian Studies 2023 Т. 11 С. 241–270
Как практикующие историки приходят к тем или иным убеждениям? Как отличить «гипотетическое» от «доказанного»? Почему в определенный момент те или иные интерпретации находят всеобщую поддержку в научном сообществе, а другие нет? И как в дальнейшем общепризнанные интерпретации могут быть опровергнуты? Эти вопросы находятся в центре внимания этой статьи, но рассматриваются не отвлеченно, на уровне теории, ...
Добавлено: 23 ноября 2023 г.
Автоматическая верификация многосторонних соглашений и планирование отправки сообщений в системах распределенного реестра
Федотов И. А., Хританков А. С., Обидаре М. Д., Программная инженерия 2022 № 4 С. 200–208
Многосторонние соглашения используются в системах распределенного реестра и блокчейн-сетях для согласования изменений в системе. Если один из участников сети предлагает транзакцию на запись, то сначала ее должны подтвердить определенные участники сети. Многостороннее соглашение, или консенсус, определяет состав этих участников. На основе предыдущих ответов можно посчитать вероятность подтверждения транзакции для каждого из участников. В настоящей работе ...
Добавлено: 20 сентября 2022 г.
InnoChain: распределенный реестр для индустриального применения с формальной верификацией на всех уровнях реализации
Кухаренко В. А., Зиборов К. В., Садыков Р. Ф. и др., Моделирование и анализ информационных систем 2020 Т. 27 № 4 С. 454–471
Степень применения методов формальной верификации в индустриальных проектах всегда была ограничена. Распространение систем распределенного реестра (СРР), известных также как блокчейн, быстро меняет ситуацию. Поскольку основной областью применения СРР является автоматизация финансовых транзакций, свойства предсказуемости и надежности являются критическими при реализации таких систем. Реальное поведение СРР определяется выбранным протоколом консенсуса, свойства которого нуждаются в строгой спецификации ...
Добавлено: 31 мая 2021 г.
Using an extension of CTL* for specification and verification of sequential reactive systems
Гнатенко А. Р., Захаров В. А., Системная информатика 2020 Vol. 17 P. 21–32
Последовательные реагирующие системы, такие как контроллеры, системные драйверы, компьютерные интерпретаторы, работают с двумя потоками данных и преобразуют входные потоки данных (управляющие сигналы, инструкции) в выходные потоки управляющих сигналов (инструкции, данные). Конечные преобразователи широко используются в качестве подходящей формальной модели для подобных систем обработки информации. Поскольку вычисления преобразователей протекают во времени, темпоральная логика, очевидно, может использоваться ...
Добавлено: 9 ноября 2020 г.
Научный подход и универсальная этика
Сторчевой М. А., В кн.: Мораль и универсальностьВып. 3.: М.: Издательский дом "Гуманитарий", 2020. С. 147–160.
В этой статье мы обосновываем тезис о том, что универсальная этика может быть построена на основе научного подхода, что позволяет обосновать ее универсальность и спасти от методологических обвинений в субъективизме или релятивизме. Вначале мы объясняем выбор критериев научности: 1) точная терминология, 2) корректный логический анализ, 3) эмпирическая верификация, 4) точность эмпирических измерений. Затем мы выстраиваем ...
Добавлено: 31 октября 2020 г.
Научно-технический вклад В. В. Липаева в инженерию разработки надежных и качественных программных систем
Позин Б. А., Васенин В. А., Лаврищева Е. М. и др., Программная инженерия 2018 Т. 9 № 9 С. 387–392
Статья посвящена памяти одного из основателей инженерии разработки комплексов программ и систем в СССР и в Российской Федерации — Владимира Васильевича Липаева, со дня рождения которого в 2018 г. исполнилось 90 лет. Более 60 лет В. В. Липаев руководил работами по созданию крупных программных комплексов в интересах оборонной промышленности и других стратегически важных отраслей национальной экономики. ...
Добавлено: 11 декабря 2019 г.
«Пороги» между доходными группами: результаты анализа рисков бедности
Слободенюк Е. Д., В кн.: Модель доходной стратификации российского общества: динамика, факторы, межстрановые сравнения.: Издательство Нестор-История, 2018. Гл. 1.4 С. 93–116.
Глава посвящена вопросу того, какой именно должна быть черта бедности в ее монетарном относительном выражении в доле от медианы среднедушевых доходов по стране. В западных исследованиях, посвященных проблематике доходной стратификации, используются различные величины, колеблющиеся в пределах 0,5 - 0,75 от медианы среднедушевого дохода. На основе данных о рисках бедности делается вывод о том, что черта ...
Добавлено: 16 апреля 2019 г.
Компонентная верификация операционных систем
Кулямин В. В., Петренко А. К., Хорошилов А. В., Труды Института системного программирования РАН 2018 Т. 30 № 6 С. 367–382
В работе рассматриваются полученные недавно результаты на пути к полномасштабной верификации промышленно используемых операционных систем (ОС). Таковыми считаются не системы, разработанные в целях демонстрации определенной исследовательской идеи, а ОС, активно используемые в каких-то областях экономики и управленческой деятельности и развиваемые на протяжении значительного времени. Предлагается декомпозиция заявленной цели верификации промышленной ОС в целом на задачи ...
Добавлено: 14 февраля 2019 г.
Генератор тестовых программ для архитектуры RISC-V на основе инструмента MicroTESK
Татарников А. Д., Камкин А. С., Проценко А. С. и др., Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС) 2018 № 2 С. 2–8
В работе рассматривается генератор тестовых программ, предназначенный для верификации микропроцессоров с архитектурой RISC-V. Генератор разработан на основе инструмента MicroTESK и состоит из формальных спецификаций архитектуры RISC-V и архитектурно независимого ядра. Спецификации задают синтаксис и семантику команд. Ядро реализует техники построения последовательностей команд и генерации данных. Генерация осуществляется на основе шаблонов, описывающих структурные и поведенческие свойства программ. Инструмент позволяет расширять ...
Добавлено: 30 октября 2018 г.
Proceedings of 9th Workshop “Program Semantics, Specification and Verification: Theory and Applications" (PSSV-2018), Yaroslavl, Russia, June 21-22, 2018
Yaroslavl: Ярославский государственный университет им. П.Г. Демидова, 2018.
Добавлено: 26 октября 2018 г.
Обработка экспериментальных данных при верификации компонентов физических систем: оценка качества тестовых последовательностей
Лапутенко А. В., Лопез Х. Е., Евтушенко Н. В., Известия высших учебных заведений. Физика 2017 Т. 60 № 11 С. 146–151
Данная статья является продолжением исследований по построению качественных верификационных тестов для проверки цифровых компонентов, используемых в различных физических системах, таких, как, например, встраиваемые датчики и элементы, используемые для передачи данных. Для экспериментальных исследований выбраны схемы из пакета бенчмарок B01-B10 (ITC’99 benchmarks (Second Release)), которые представляют собой компоненты физических систем, спроектированных для различных приложений. Тестовые последовательности ...
Добавлено: 11 августа 2018 г.
A Scientific Approach to Ethics: Developing Greater Respect for Ethics in Business and Society
Сторчевой М. А., Switzerland: Palgrave Macmillan, 2018.
Добавлено: 26 января 2018 г.
Средства функциональной верификации микропроцессоров
Татарников А. Д., Камкин А. С., Чупилко М. М. и др., Труды Института системного программирования РАН 2014 Т. 26 № 1 С. 149–200
Обеспечение корректности микропроцессоров и другой микроэлектронной аппаратуры является фундаментальной проблемой, для решения которой применяют разнообразные средства функциональной верификации. В отличие от программ, ошибки в которых исправляются сравнительно просто, дефекты в интегральных схемах (конструктивные и производственные) не могут быть устранены. Несмотря на то, что постоянно совершенствуются системы автоматизированного проектирования (САПР), инструменты генерации тестов и методы анализа ...
Добавлено: 11 декабря 2017 г.
Верификация и анализ вариабельных операционных систем
Кулямин В. В., Лаврищева Е. М., Мутилин В. С. и др., Труды Института системного программирования РАН 2016 Т. 28 № 3 С. 189–208
В данной работе рассматриваются проблемы верификации и анализа сложных операционных систем с учетом их вариабельности, или наличия большого количества разнообразных конфигураций. Исследуются методы, позволяющие преодолеть эти проблемы, проводится их обзор и классификация. Выделены классы методов, использующих для анализа инструменты, не учитывающие вариабельность, и выборки вариантов системы и методов, использующих специализированные инструменты, учитывающие вариабельность. Как наиболее ...
Добавлено: 28 августа 2017 г.
Трансляция вложенных сетей Петри в классические сети Петри для верификации разверток
Ермакова В. О., Ломазова И. А., Труды Института системного программирования РАН 2016 Т. 28 № 4 С. 115–136
Вложенные сети Петри являются одним из удобных формализмов для моделирования и анализа поведения распределенных мультиагентных систем. Они естественным образом представляют структуру мультиагентных систем, так как фишки в системной сети сами являются классическими сетями Петри и могут иметь автономное поведение. Мультиагентные системы являются системами с высоким уровнем параллелизма. При верификации таких систем методами проверки модели (model ...
Добавлено: 21 октября 2016 г.
Проблемы разработки перспективных микро- и наноэлектронных систем Сборник трудов конференции (МЭС-2016). Сборник трудов
М., Зеленоград: ИППМ РАН, 2016.
Часть II сборника научных трудов составлена по материалам секций 4 и 5 ("Верификация и тестирование", "Высокопроизводительные вычислительные микроэлектронные системы") VII Всероссийской научно-тенчнической конференции "Проблемы разработки перспективных микро- и наноэлектронных систем -2016" (Москва, Зеленоград 03.10 - 07.10.2016г.). Сборник трудов". Представленные работы выполнены научными сотрудниками и аспирантами РАН, специалистами работающих в России научно-производственных организаций, преподавателями, научными сотрудниками, ...
Добавлено: 27 сентября 2016 г.
  • О ВЫШКЕ
  • Цифры и факты
  • Руководство и структура
  • Устойчивое развитие в НИУ ВШЭ
  • Преподаватели и сотрудники
  • Корпуса и общежития
  • Закупки
  • Обращения граждан в НИУ ВШЭ
  • Фонд целевого капитала
  • Противодействие коррупции
  • Сведения о доходах, расходах, об имуществе и обязательствах имущественного характера
  • Сведения об образовательной организации
  • Людям с ограниченными возможностями здоровья
  • Единая платежная страница
  • Работа в Вышке
  • ОБРАЗОВАНИЕ
  • Лицей
  • Довузовская подготовка
  • Олимпиады
  • Прием в бакалавриат
  • Вышка+
  • Прием в магистратуру
  • Аспирантура
  • Дополнительное образование
  • Центр развития карьеры
  • Бизнес-инкубатор ВШЭ
  • Образовательные партнерства
  • Обратная связь и взаимодействие с получателями услуг
  • НАУКА
  • Научные подразделения
  • Исследовательские проекты
  • Мониторинги
  • Диссертационные советы
  • Защиты диссертаций
  • Академическое развитие
  • Конкурсы и гранты
  • Внешние научно-информационные ресурсы
  • РЕСУРСЫ
  • Библиотека
  • Издательский дом ВШЭ
  • Книжный магазин «БукВышка»
  • Типография
  • Медиацентр
  • Журналы ВШЭ
  • Публикации
  • http://www.minobrnauki.gov.ru/
    Министерство науки и высшего образования РФ
  • https://edu.gov.ru/
    Министерство просвещения РФ
  • http://www.edu.ru
    Федеральный портал «Российское образование»
  • https://elearning.hse.ru/mooc
    Массовые открытые онлайн-курсы
  • НИУ ВШЭ1993–2026
  • Адреса и контакты
  • Условия использования материалов
  • Политика конфиденциальности
  • Правила применения рекомендательных технологий в НИУ ВШЭ
  • Карта сайта
Редактору