Толерантный синтаксический анализ используется для разбора структуры областей программы, представляющих интерес в контексте определённой задачи. В то время как эти области должны быть подробно описаны в толерантной грамматике языка, описание остальных частей программы может быть менее детальным, в результате парсер толерантен по отношению к возможным вариациям нерелевантных областей. Островные грамматики — один из основных способов реализации толерантного парсинга. Термином «остров» обозначаются релевантные области кода, нерелевантный код обозначается термином «вода». Предполагается, что на написание водных правил грамматики должно тратиться как можно меньше усилий. Ранее автором настоящей работы была введена формальная концепция упрощённой грамматики, расширяющая теорию островных грамматик. Данная концепция основана на идее устранения описаний воды в грамматике путём замены их на специальный символ «Any». Для работы с упрощёнными грамматиками был модифицирован стандартный LL(1) алгоритм синтаксического анализа и разработан генератор толерантных парсеров LanD. В настоящей статье модификация, встраивающая обработку «Any», описывается для LR(1) алгоритма синтаксического анализа. В сравнении с толерантными LL(1) грамматиками, толерантные LR(1) грамматики являются более простыми для разработки и исследования ввиду того, что в них каждый остров может быть описан одним непрерывным правилом. Предложены дополнительные механизмы обработки символа «Any», приводящие ряд интуитивно корректных сценариев его использования в соответствие с формальным определением упрощённой грамматики. Для LL и LR толерантного синтаксического анализа описаны специфические механизмы восстановления от ошибок, позволяющие ещё больше сократить количество водных правил, понизить их сложность и сделать толерантную грамматику расширяемой. В разделе экспериментов представлены результаты крупномасштабного тестирования толерантных LL и LR парсеров на 9 репозиториях крупных проектов с открытым исходным кодом.

В связи с увеличением количества платформ, языков и методов, использующихся в разработке мобильных приложений, задача выработки общей технологии довольно актуальна. Графические языки упрощают разработку, позволяя представить структуру программного обеспечения в виде графических диаграмм. Кроме того, графические языки помогают избежать множества ошибок еще на начальных этапах проектирования и разработки. Графические предметно-ориентированные языки (DSL) облегчают разработку  программ путем применения абстракций конкретной предметной области. В данной работе представлен архитектурный шаблон мобильного приложения и созданный на его основе графический DSL, позволяющий описывать основную структуру мобильного приложения в терминах котнроллеров, состояний и переходов между ними. При таком подходе структура мобильного приложения будет представлена в виде различных контроллеров, связанных между собой при помощи портов и соответствующих некоторым целостным фрагментам логики. Сами контроллеры в свою очередь состоят из различных состояний, которые позволяют описать поток данных в контроллере путем соединения при помощи элемента-связи. В каждом состоянии может быть описана экранная форма, в которой содержатся графические примитивы и связанные с ними события, срабатывающие при их изменении. Кроме того, для разработанного DSL реализована автоматическую генерация кода для платформы UbiqMobile. В конце статьи приводятся демонстрационные примеры, на которых был апробирован DSL язык. В качестве первого примера приводится приложение, позволяющее пользователю посмотреть расписание электричек. Во втором приложении пользователь может войти в систему для того, чтобы получить check-in код.

Предметом данной статьи является разработка программной среды для управления интеллектуальными устройствами в режиме реального времени. Платформа обеспечивает интеллектуальное управление устройствами Интернета вещей в кибер-физических системах с использованием моделей, основанных на рекуррентных соотношениях и дифференциальных уравнениях. Платформа была разработана с использованием языка программирования Python, инфраструктуры Django и широкого набора модулей и библиотек, поддерживающих непрерывное моделирование. Программная среда также включает интерфейс прикладного программирования для спецификации поведения системы, передачи входных параметров и выходных результатов, отправки управляющих действий через веб-сервисы для системы Интернета вещей.

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

При разработке систем-на-кристалле необходимо проводить верификацию как отдельных подмодулей (контроллеров периферийных интерфейсов и коммутаторов), так и системы в целом. В статье представлен подход к разработке тестов для верификации программируемых контроллеров. Тесты разрабатываются на языке программирования C++; программирование тестируемого устройства и тестового окружения осуществляется с помощью специального программного интерфейса. Функции этого программного интерфейса реализуются в стандартной библиотеке тестового окружения; реализация зависит от структуры тестового окружения: в качестве моделируемого устройства может выступать только тестируемый контроллер, контроллер в составе блока контроллеров, или контроллер в составе полной системы-на-кристалле. Для верификации системного уровня библиотека и тестовая программа компилируются для исполнения на одном из вычислительных ядер системы-на-кристалле. При автономной верификации тестовая программа и библиотека окружения  формируют программный модуль, взаимодействующий с симулятором RTL-описания с помощью стандартного интерфейса PLI; библиотечные функции взаимодействуют с моделируемым устройством через специальный адаптер системного интерфейса; кроме того, в тестовое окружение может быть включен имитатор внешнего устройства. При таком устройстве тестового окружения одна и та же тестовая программа может проверять устройства с одним программным интерфейсом, но разными системными интерфейсами; необходимо только реализовать соответствующие адаптеры. Представленный подход позволяет запускать тестовую программу как автономный тест, так и в качестве теста интеграции на верифицируемой системе-на-кристалле. В статье описаны реализация представленного подхода и его применение в маршруте верификации микропроцессоров семейства Эльбрус.

Современные микропроцессорные системы обычно включают сложную иерархию кэш-памяти. Протоколы когерентности используются для поддержания согласованности памяти. Реализация подсистемы памяти на языке описания аппаратуры является сложной и подверженной ошибкам задачей. Обеспечение корректного функционирования подсистемы памяти, является одной из важнейших задач в процессе разработки современных микропроцессорных систем. Для этого используется функциональная верификация. В данной работе представлены некоторые подходы к верификации блоков подсистем памяти многоядерных микропроцессоров. Описаны характеристики подсистем памяти, которые необходимо учитывать в процессе верификации. Представлена общая структура тестовой системы для автономной верификации блоков подсистемы памяти. Приведена классификация типов проверяющих моделей, их преимущества и недостатки. В статье представлен подход к построению автономного окружения для верификации с использованием универсальной методологии верификации (UVM). Перечислены ограничения, которые следует учитывать при проверке блоков подсистемы памяти. Представлен алгоритм генерации входных стимулов. Для устранения неопределенности текущего состояния верифицируемого устройства в проверяющем модуле используется метод анализа «подсказок». Рассмотрен ряд других методов проверки корректности блоков подсистемы памяти, которые могут быть полезны на различных этапах разработки проекта. Представлен пример применения предложенных подходов к верификации блока HMU микропроцессоров с архитектурой Эльбрус. Приведена классификация обнаруженных и исправленных ошибок в различных подмодулях верифицируемого устройства. Представлен дальнейший план совершенствования тестовой системы.

В данной статье представлен подход к автономной верификации блока управления памятью ввода / вывода с поддержкой виртуализации. Мы представляем базовую архитектуру тестовой системы. Рассматриваются основные проблемы, возникающие при верификации IOMMU с поддержкой виртуализации. Одной из ключевых проблем стало формирование страниц таблицы трансляции. Количество таблиц трансляции зависит от режима работы IOMMU и типа трансляции. В качестве решения этой проблемы предложен подход к динамической генерации таблиц трансляции. Представлен алгоритм формирования страниц таблиц трансляции в генераторе. Решается проблема проверки трансляции виртуального адреса в физический с использованием двухуровневых таблиц трансляций. Рассмотрены особенности реализации эталонной модели. Описаны эталонная модель и тестовая система, которые использовались для верификации микропроцессора IOMMU с архитектурой 6-го поколения «Эльбрус». Представлены методы связи между тестовой системой и моделью IOMMU. Рассматриваются результаты проверки IOMMU.

В данной статье представлен модульный подход, позволяющий снизить трудозатраты на технологическую подготовку мелкосерийного металлообрабатывающего производства. Его идея состоит в том, чтобы формализовать технологические процессы, позволяя генерировать их и их документацию из предварительно подготовленных параметризованных шаблонов, хранящихся в специальной базе данных. Обрабатываемые детали представлены в виде структур их основных геометрических компонентов. Для шаблона операций обработки для каждого компонента фиксируются символические параметры, характеризующие используемую заготовку, параметры режущих инструментов, режимы обработки и т. д. Результатом формализации является автоматически генерируемый технологический маршрут в виде диаграммы MSC, кодирующей его как последовательность макроопераций для станков. Эта символическая модель адаптируется к конкретной изготавливаемой детали путем замены символических переменных определяемыми технологом значениями. Диаграмма MSC дополняется результатами расчётов времени и стоимости исполнения технологических маршрутов, что позволяет выбрать из них наиболее эффективный. Корректность технологических маршрутов обеспечивается в процессе символьной верификации путем проверки допустимых диапазонов параметров диаграммы MSC, а также проверки правильности порядка и совместимости операций в последовательности. Результатом всего процесса, полученного из диаграммы MSC, является набор технологической документации на подготовку производства, который, в частности, включает в себя набор операционных карт, а также отлаженный график производства после его цифрового моделирования с учётом реальных ресурсов мастерской. По оценкам технологов, после применения описанной автоматизации время на подготовку документации для деталей средней сложности сокращается с нескольких недель до 1-2 дней.

В наши дни электронная коммерция (ЭК) показывает беспрецедентные темпы роста во всем мире, вовлекая в эту деятельность миллионы людей на всех континентах. В то же время, ЭК создает почву для злонамеренных действий, что требует особого внимания и контроля. Одним из способов минимизации таких угроз является использование репутационных систем для отслеживания степени доверия в среде пользователей сети. Большинство существующих репутационных систем основаны на сборе отзывов относительно проведенных транзакций, и они, как правило, работают с представленными в виде чисел откликами клиентов (в частности, может использоваться привычная целочисленная шкала 0..5). В целом, понятия доверия и репутации являются примерами неопределенных (неточных) информационных данных, характерных для сферы электронной коммерции. Мы предлагаем использовать аппарат нечеткой логики для формального представления пользовательских отзывов, выражающих степень удовлетворенности результатом совершенных транзакций. В работе представлен краткий сравнительный анализ наиболее известных репутационных систем, таких как EigenTrust, HonestPeer, Absolute Trust, PowerTrust и PeerTrust. С учетом выделенных в результате анализа критериев (скорость сходимости, устойчивость (робастность), наличие гиперпараметров), проведенная серия компьютерных экспериментов позволила эмпирически выделить PeerTrust как наиболее устойчивый и масштабируемый алгоритм из числа рассмотренных. При наличии ограничений в отношении имеющихся данных, подготовлены реализации (Python 3.7) и проанализированы результаты, связанные с особенностями поведения нечетких версий алгоритма PeerTrust на основе нечетких множеств типа-1 (T1FS) и интервальных нечетких множеств второго типа (IT2FS).

Существующие на сегодняшний день инструменты дедуктивной верификации позволяют успешно доказывать корректность функций, написанных на высокоуровневых языках, таких как C или Java. Однако для критического ПО этого может быть недостаточно, поскольку даже полностью верифицированный код не может гарантировать корректной генерации машинного кода компилятором. На данный момент разработчикам таких систем приходится принимать предположение о корректности компилятора, что, однако, является крайне нежелательным, но неизбежным поступком в силу отсутствия полноценных систем формальной верификации машинного кода. Стоит также отметить, что верификация машинного кода человеком напрямую является крайне трудоёмкой задачей из-за высокой сложности и больших объёмов машинного кода. Одним из подходов, позволяющих упростить верификацию машинного кода – является автоматическая дедуктивная верификация с переиспользованием формальной спецификации функции языка высокого уровня. Формальная спецификация функции состоит из спецификации пред- и постусловия, а также инвариантов циклов, позволяющих определить какие условия сохраняются на каждой итерации цикла. При компиляции программы в машинный код пред- и постусловия сохраняются что, однако нельзя сказать об инвариантах циклов. Этот факт является одной из основных проблем автоматической верификации машинного кода с циклами. Другой немаловажной проблемой является то, что локальные переменные функций высокого уровня могут иметь ‘позиции’ как на регистры, так и на память на уровне машинного кода. Если абстрагироваться от конкретного компилятора, то не существует строгих правил сопоставления локальных переменных их позициям, а процедура верификации инвариантов циклов, тем не менее требует того, чтобы локальным переменным были сопоставлены конкретные позиции. В данной работе приводится подход к решению этих проблем, а также рассматриваются альтернативные пути решения, предложенные в аналогичных исследованиях.

При проектировании модулей цифровой аппаратуры могут возникать конфликты доступа к данным. Одним из способов их выявления на ранних стадиях проектирования является статический анализ описаний цифровой аппаратуры (или HDL-описаний). В данной статье описывается метод поиска конфликтов доступа к данным в HDL-описаниях. Метод реализован в инструменте Retrascope и ориентирован на конфликты следующих типов: одновременные чтение и запись; одновременная запись; обращение к неинициализированным данным; отсутствие чтения между двумя актами записи. Конфликты задаются в виде условий (assertion) на внутренние переменные. Входное HDL-описание автоматически транслируется в формальную модель на языке, являющемся входным для инструмента проверки моделей nuXmv. Трансляция включает следующие этапы: 1) предварительная обработка; 2) построение графа потока управления; 3) трансформация графа потока управления в решающую диаграмму охраняемых действий (GADD-модель); 4) трансляция GADD-модели в формат инструмента nuXmv. Условия возникновения конфликтов строятся автоматически на основе статического анализа GADD-модели и передаются инструменту проверки моделей nuXmv. Найденные контрпримеры (последовательности значений входных сигналов, приводящие к достижению конфликта) автоматически транслируются инструментом Retrascope в тесты, которые могут быть исполнены на симуляторе. Предложенный метод поиска конфликтов был применен к ряду открытых тестовых наборов и модулей – Texas-97, Verilog2SMV, VCEGAR, mips16. Были выявлены потенциальные конфликты для всех указанных категорий. В качестве направлений дальнейших исследований рассматриваются вынос условий конфликтов на уровень входных сигналов (и получение, таким образом, сведений о протоколах взаимодействия между модулями), а также генерация встроенных проверок в коде HDL-описаний.

Задача маршрутизации – одна из широко известных задач комбинаторной оптимизации. Она состоит в отыскании оптимального множества маршрутов для транспортных средств с целью однократного обслуживания определенного множества клиентов. В данной работе исследуется подвид задачи маршрутизации – задача маршрутизации с ограничением по грузоподъемности, в которой каждое транспортное средство имеет свою грузоподъемность. Задача является NP-трудной, поэтому вместо точных алгоритмов решения исследуются только эвристические алгоритмы, позволяющие получить приближенные решения за полиномиальное время. Задача работы – провести экспериментальное исследование точности решения различных конструктивных эвристик, так как в других источниках не было найдено подобных сравнений.  В большинстве случаев, лидером можно признать эвристику «Clarke and Wright Savings», однако существуют отдельные наборы данных, описанные в тексте, на которых лучше работают другие алгоритмы. Также в статье рассмотрены и другие интересные факты. В целом работа проделана с целью дальнейшего использования полученных знаний в экспериментальном исследовании наиболее известных и современных метаэвристических алгоритмов решения задачи маршрутизации с ограничением по грузоподъемности, для которых будут получены предварительные решения на основе выявленных лучших эвристических методов конструирования маршрута.

Технология распределенного реестра блокчейн становится все более популярной и находит применение в различных областях, в том числе и в финансовых технологиях. Многие блокчейн-платформы поддерживают функциональность смарт-контрактов, которые предназначены для автоматизации заключения договоров. Известны примеры, где ошибки или небрежности в коде смарт-контракта приводят к потере активов, например, из-за атаки злоумышленника или непонимания разработчиком особенностей блокчейн-платформы. На сегодняшний день существует множество различных подходов, которые позволяют сделать смарт-контракты безопаснее. Среди них инструменты анализа кода, модели вычислений и семантики языков программирования смарт-контрактов. В этой работе мы приводим обзор языков программирования смарт-контрактов, принципов их построения, а также потенциальные ошибки в программе смарт-контракта. Основная цель этого обзора — рассмотреть текущее на момент написания статьи состояние языков смарт-контрактов и возможные направления для будущих исследований, а также показать подходы, используемые сообществом для создания безопасного и удобного (с точки зрения абстракции) языка. Характеристики множества языков, такие как: уровень абстракции, парадигма, Тьюринг-полнота, проект, где язык используется, инструменты для анализа кода, система ограничения и главные особенности — были рассмотрены и сведены в таблицу. Предоставлена дополнительная информация о языках, например, о модели выполнения. Также мы кратко описали и разделили все найденные нами уязвимости по источникам их возникновения.

В связи с большими объёмами кода в современных программных продуктах, в программах всегда существует целый набор малозаметных ошибок или дефектов, которые сложно обнаружить при повседневном использовании или в ходе обычного тестирования. Многие такие ошибки могут быть использованы в качестве потенциального вектора атаки, если они могут быть эксплуатированы удалённым пользователем посредством манипуляций над входными данными программы. В данной работе представлен подход к автоматическому обнаружению уязвимостей безопасности с использованием межпроцедурного статического анализа помеченных данных. Цель данного исследования – разработка инфраструктуры анализа помеченных данных, применимой для обнаружения уязвимостей в программах на языках C и C++ и расширяемой при помощи отдельных детекторов. Этот инструмент основывается на алгоритме решения задачи Межпроцедурных, Конечных, Дистрибутивных Подмножеств (IFDS) при помощи её сведения к специальной задаче о достижимости на графе и способен выполнять межпроцедурный, чувствительный к контексту, нечувствительный к путям анализ программ, представленных в виде LLVM-биткода. Анализа помеченных данных недостаточно для получения хороших результатов, поэтому улучшения существующих методов, мы предлагаем дополнить его ещё одним этапом анализа, который основан на статическом символьном выполнении. Для фильтрации результатов первого этапа выполняется анализ, чувствительный к путям и учитывающий размеры регионов памяти. Оценка результатов была проведена на Juliet Test Suite и проектах с открытым исходным кодом, имеющих подходящие публично известные уязвимости из базы данных CVE.

Криптографические протоколы являются ядром любой защищенной системы. С их помощью передаются данные, которые нуждаются в защите от третьих лиц. Как правило, криптографический протокол разрабатывается, анализируется с использованием средств формальной верификации и, если он безопасен, реализуется на языке программирования, на котором разрабатывается система. Однако при практической реализации криптографического протокола могут возникать ошибки из-за человеческого фактора, предположений, которые необходимы для возможности реализации протокола, что влечет за собой подрыв его безопасности. Таким образом, оказывается, что сам протокол изначально считался безопасным, но его реализация на самом деле небезопасна. Кроме того, формальная верификация использует довольно абстрактные понятия и не позволяет полностью проанализировать протокол. В данной статье представлен алгоритм анализа исходного кода языка программирования C # для извлечения структуры криптографических протоколов. Описаны особенности реализации протоколов на практике. Алгоритм основан на определении ключевых областей кода, содержащих специфические для криптографических протоколов конструкции, и определении цепочки преобразований переменных из состояния отправки или получения сообщений до их начальной инициализации с учетом возможных криптографических преобразований для составления дерева, из которого будет извлечена упрощенная структура криптографического протокола. Алгоритм реализован на языке программирования C# с использованием синтаксического анализатора Roslyn. В качестве примера представлен криптографический протокол, который содержит основные операции и функции, а именно: асимметричное и симметричное шифрование, хеширование, подпись, генерация случайных чисел, конкатенация данных. Работа анализатора показана с использованием этого протокола в качестве примера. Описана будущая работа.

Сильно ветвящиеся деревья являются одним из наиболее популярных решений для индексирования больших объёмов данных. Наиболее распространённой разновидностью сильно ветвящихся деревьев являются B-деревья. Существуют различные модификации B-деревьев, в том числе, рассматриваемые в настоящей работе B⁺-деревья, B^*-деревья и B^*+-деревья, однако данные модификации не поддерживаются по умолчанию в популярной реляционной СУБД с открытым исходным кодом SQLite. Данная работа выполняется на основе проведённого ранее исследования эффективности сильно ветвящихся деревьев в задаче индексирования структурированных данных, с использованием разработанной в рамках него C++-библиотеки структур данных – сильно ветвящихся деревьев. В этом исследовании было разработано B^*+-дерево как структура данных, совмещающая в себе основные свойства B⁺-дерева и B^*-дерева. Также в исследовании были измерены эмпирические вычислительные сложности различных операций над B-деревом и его модификациями и объём потребляемой данными операциями оперативной памяти. Целью настоящей работы является разработка расширения для реляционной СУБД SQLite, позволяющего использовать модификации B-дерева (B⁺-дерево, B^*-дерево и B^*+-дерево) в качестве индексирующих структур данных в РСУБД SQLite. Модификации базовой структуры данных были разработаны в виде C++-библиотеки. Данная библиотека подключается к SQLite, используя разработанный для неё в рамках настоящей работы API на языке C. Расширение для SQLite также реализует новый алгоритм выбора индексирующей структуры данных (одной из модификаций B-дерева) для заданной таблицы в базе данных. Предложенное расширение используется компонентом SQLite EventLog библиотеки LDOPA алгоритмов и структур данных для process mining. Кроме того, проведён эксперимент по сравнению эмпирической вычислительной сложности операций на деревьях разных типов в разработанном расширении для SQLite.

В данной статье представлен подход к описанию клеточных автоматов с использованием тензоров. Такой подход позволяет привликать различные фреймворки для огранизации расчетов на высокопроизводительных графических видеокартах, т.е. для автоматического построения параллельных программных реализаций клеточных автоматов. В нашей работы мы используем фреймворк TensorFlow для организации вычислений на графических видеокартах NVIDIA. В качестве примера клеточного автомата мы рассмотрели игру «Жизнь». Эффект от описанного подхода к программной реализации клеточных автоматов оценён экспериментально.

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