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

Методы и инструменты автоматической статической верификации позволяют выявить все ошибки искомых видов в целевых программах при выполнении определенных предположений даже в условиях отсутствия полных моделей и формальных спецификаций. Эта возможность является основой предлагаемого в работе метода инкрементального построения спецификаций моделей окружения и требований для подсистем монолитного ядра операционных систем. Данный метод был реализован в системе статической верификации Klever и применен для проверки подсистемы поддержки терминальных устройств ядра ОС Linux.

В статье авторами рассматриваются результаты дедуктивной верификации набора из 26 библиотечных функций ядра ОС Linux с помощью стека инструментов AstraVer. В набор включены преимущественно функции, работающие с данными строкового типа. Целью верификации является доказательство свойств функциональной корректности. В статье рассматриваются аналогичные работы по верификации, сравниваются полученные результаты, рассматривается ряд проблем, с которыми сталкивались авторы предыдущих работ, в том числе проблемы, с которыми удалось справится в рамках данной работы и те, которые все ещё препятствуют успешной верификации. Также предлагается методология разработки спецификаций, примененная для рассматриваемого набора функций, которая включает некоторые шаблонные приёмы разработки спецификаций. Авторам удалось доказать полную корректность двадцати пяти функций. В статье приведены результаты доказательства полученных условий верификации каждой функции с помощью нескольких современных SMT-солверов.

Работа посвящена решению задачи декомпиляции одного из разновидностей формата DCU - файлов .dcuil, создаваемых компиляторами тех версий Delphi, которые работали для платформы .NET. Разработан метод решения этой задачи, состоящий из ряда этапов: синтаксический анализ кода CIL; формирование графа потока управления; генерация промежуточного представления; структурирование графа потоков управления; анализ потоков данных с учётом семантики команд CIL; улучшение промежуточного представления с учётом особенностей работы компилятора Delphi; генерация кода.

Разработка программного обеспечения является сложным и подверженным ошибкам процессом. В целях снижения сложности разработки ПО создаются сторонние библиотеки. Примеры исходных кодов для популярных библиотек доступны в литературе и интернет-ресурсах. В данной работе представлена гипотеза о том, что большинство подобных примеров содержат повторяющиеся шаблоны. Более того, данные шаблоны могут быть использованы для построения моделей, способных предсказать наличие (либо отсутствие) недостающих вызовов определенных библиотечных функций с использование машинного обучения. В целях проверки данной гипотезы была реализована система, реализующая описанный функционал. Экспериментальные исследования, проведенные на примерах для библиотеки OpenGL, говорят в поддержку выдвинутой гипотезы. Точность результатов достигает 80%, при условии рассмотрения уже первых 4-х ответов, предлагаемых системой. Можно сделать вывод о том, что данная система при дальнейшем развитии может найти индустриальное применение.

Разыменование нулевого указателя остаётся одной из основных проблем в современных объектно-ориентированных языках. Очевидное добавление ключевых слов, чтобы различать между всегда ненулевыми и возможно нулевыми ссылками, оказывается недостаточным во время инициализации объекта, когда некоторые поля, объявленные всегда ненулевыми, могут временно быть нулевыми до окончания инициализации. Существует несколько подходов к решению проблемы инициализации объекта. Каким образом их можно сравнить практически? Являются ли реализации обоснованными? Данная работа представляет набор примеров, выделяя сценарии использования из публикаций по теме и библиотек с открытым кодом, и объясняет стоящие за ними критерии. Затем она обсуждает ожидаемые результаты для выбранного набора инструментов, производящих проверки безопасности нулевых ссылок для Eiffel, Java и Kotlin, и завершается фактическими результатами, демонстрирующими незрелость решений.

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

В данной работе рассматриваются проблемы масштабируемости проекта Keystone - центрального сервиса авторизации и аутентификации облачной платформы Openstack и новый принцип построения сервиса, позволяющий избегать этих проблем. В более ранних работах был предложен подход к масштабированию Openstack Keystone путем отказа от использования СУБД MySQL/MariaDB и PostgreSQL в качестве хранилища данных сервиса в пользу распределенных NoSQL решений. Данная работа представляет полноценную реализацию сервиса, обеспечивающего полную функциональность Openstack Keystone API V3, на базе API Gateway и использования Apache Cassandra.

Для описания случайных сетей используется модель случайного графа Эрдёша-Реньи . При исследовании современных случайных сетей часто требуется определить размер максимальной плотной подсети. В настоящей статье приводятся оценки максимального размера c-плотного подграфа, асимптотически почти наверно содержащегося в случайном графе . Было показано, что при , - асимптотически почти наверно c-плотный; получены верхняя и нижняя оценки размера максимального -плотного подграфа, асимптотически почти наверно. содержащегося в ; а при получена оценка сверху на размер максимального с-плотного подграфа асимптотически почти наверно содержащегося в .

В 2012 году М. А. Трушников предложил принципиально новый онлайновый алгоритм упаковки прямоугольников в полосу, а в 2013 году в [3] была получена оценка точности алгоритма в среднем, равной математическому ожиданию незаполненной прямоугольниками площади, равная . Ранее известная оценка была существенно улучшена. В настоящей работе данная оценка улучшена до , а также алгоритм Трушникова обобщён на случай упаковки прямоугольников в полос, , с сохранением оценки .

В связи с развитием ветроэнергетики и строительством новых ветропарков в РФ возникает потребность в решении ряда прикладных задач и разработке эффективных методик расчета элементов ветроустановок. Одно из направлений в задачах механики сплошной среды связано с задачами аэроупругости. В данной статье показана возможность решения связанной задачи аэроупругости с использованием программного комплекса на базе свободного программного обеспечения OpenFOAM и Code_Aster. На примере лопасти ветроустановки длиной 61.5 метра рассмотрены методики решения задач статической и динамической аэроупругости, в которых расчет обтекания лопасти дозвуковым набегающим потоком воздуха производится в пакете OpenFOAM (решатели simpleFOAM и pimpleFOAM), а расчет напряженно-деформированного состояния лопасти производится в пакете Code_Aster. В статье приводятся блок-схемы для трех различных подходов решения задачи аэроупругости, примеры скриптов и командных файлов для передачи данных между пакетами в процессе расчета. Контрольно-объемная сетка, состоящая их гексаэдральных элементов, для расчета обтекания лопасти построена в пакете OpenFOAM, конечно-элементная сетка, состоящая из треугольных оболочечных элементов первого порядка, для расчета напряженно-деформированного состояния построена в пакете Salome-Meca. Результаты расчета представлены в форме полей для давления и скорости; зависимостей для невязкок давления, скорости, турбулентной вязкости; проекций аэродинамической силы от времени; эпюр перемещения и напряжения; значений давления и перемещения для двух точек на поверхности лопасти от времени. Расчеты выполнены с использованием ресурсов web-лаборатории UniHUB ИСП РАН.

Представлен программный пакет для расчета параметров трехмерных стационарных и нестационарных потоков газа в сложных устройствах. Модель математического потока, используемая в пакете, основана на усредненных по Рейнольдсу уравнениях Навье-Стокса для двухкомпонентной равновесной турбулентной среды и двухпараметрической полуэмпирической модели турбулентности. Описана численная реализация программного пакета для моделирования трех сложных потоков в современных устройствах.

В этой статье мы представляем методы Surface Flow Image Velocimetry (SFIV), являюшиеся практическим расширением метода Velocimetry Image Particle Image (PIV). В частности, этот метод позволяет оценивать поведение поверхностного потока для комплексного течения. SFIVпозволяет измерять сложные поля поверхностной скорости для инженерных приложений. Целью этой работы было применение метода SFIV для определения полей скоростей и гидравлической эффективности решетчатого водоприемника. Сравнивались результаты программ Digiflow и PIVlab, способных коррелировать изображения.

Статья описывает разработку и тестирование модификации решателя для гиперзвукового реагирующего течения в среде численного моделирования OpenFOAM. Модификация создается для моделирования взаимодействия между течением и приложенным постоянным магнитным полем. Цель разработки - создать численный инструментарий для исследования концепции магнитогидродинамического управления потоком и его возможных применений. Создаваемое приложение использует математическую модель на основе уравнений Навье-Стокса, дополненных необходимыми вспомогательными моделями для описания сопряженных процессов. Тестирования решателя проводилось на задачах, демонстрирующих основные возможности созданного приложения в моделировании высокоскоростных МГД-течений различных режимов. Тестовые примеры представляют собой задачи обтекания двумерных плоско и цилиндрически симметричных тел, имеющих форму, характерную для аппаратов, для которых известны потенциальные способы применения МГД управления. Исследовалось влияние выбора модели электропроводимости на результаты численного моделирования. Сравнение результатов показало зависимость важности выбора модели электропроводимости от разреженности рассматриваемого газового потока.

В статье представлен трехмерный численный анализ структуры поля течения при прорыве плотины в масштабах лаборатории путем. Численные вычисления основывались на методе конечных объемов (Finite Volume Method, FVM), OpenFOAM. В численной модели турбулентность обрабатывается с применением методологии RANS, а метод жидких объёмов (VOF, Volume of Fluid) используется для отслеживания свободной поверхности воды. Результаты вычислений оцениваются на основе экспериментальных данных. Для валидации численной модели используются измерения глубины и давления воды. Результаты показывают, что численные вычисления удовлетворительно воспроизводят изменения этих переменных во времени.

В этой статье мы описываем метод, который представляет собой композицию метода конечных объемов (finite volume method, FVM) и метода адаптивного измельчения расчётной сетки (adaptive mesh refinement, AMR). Мы используем его для решения проблемы масляной смазки объема внутренней полости главной передачи автомобиля. Вычислительный алгоритм реализован с использованием параллельной библиотеки OpenFOAM, которая предоставляет структуры данных и подпрограммы для работы с методами конечных объемов и адаптивной сетки. Эта библиотека поддерживает параллелизм на основе OpenMPI. В статье представлены результаты численного моделирования.