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

Любая современная интегрированная среда разработки (IDE) должна предоставлять разработчикам программного обеспечения сервисы для трансформации кода. Такие сервисы могут использоваться как для рефакторинга программы с целью улучшения её качества, так и для быстрого исправления синтаксических ошибок в исходном коде. Данная работа предлагает технологию разработки подсистемы, которая позволяет создавать такие сервисы для различных IDEs и языков программирования. Предложен способ трансформации дерева Program Structure Interface (PSI) – специальной структуры данных, предоставляющей API для разработки IDE-сервисов. Помимо этого, предложен способ генерации типов для PSI сообразно синтаксису поддерживаемого языка программирования. Подход разработан для мультиязыковой платформы, создаваемой в рамках крупной технологической компании. На его основе были разработаны сервисы по модификации исходного кода для двух сред разработки – Java IDE и Python IDE.

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

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

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

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

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

Ситуация отказа в обслуживания регулярных выражений (REDoS) возникает в случае высокой вычислительной сложности сопоставления строки с выражением и встречается во многих библиотеках регулярных выражений таких языков, как PYTHON, JAVASCRIPT, C++. В данной статье рассматривается класс регулярных выражений, которые создают угрозу возникновения REDoS, однако не распознаются как уязвимые рядом существующих программных систем. Предлагается производить оценку степени неоднозначности таких выражений посредством комбинирования проверки на строгую звёздную нормальную форму и анализа трансформационного моноида автомата Глушкова, построенного по входному регулярному выражению. Эксперименты показывают, что данный подход оказывается эффективен при оценке полиномиальных неоднозначностей в регулярных выражениях со сложной структурой перекрытий.

Мы представляем простую реализацию упрощенного императивного языка программирования с прямым доступом к памяти и адресной арифметикой, а также простой статический анализатор утечек памяти. Наше исследование продолжает линию исследований, предпринятых (в Университете Иннополис в 2016-2022 годах) по исчислению алиасов для императивных языков программирования с разрешимой арифметикой указателей, но отличается моделью адресации памяти — мы изучаем сегментированную модель памяти вместо линейной.

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

Зачастую инструмент формальной верификации моделей программ не может получить вердикт за ограниченное время из-за комбинаторного взрыва пространства состояний. Чтобы найти ошибки в верифицируемой программе за выделенное время, может быть проанализирована упрощённая её версия. В этой работе представлены алгоритмы DD**, основанные на подходе Delta Debugging, с помощью которых производится перебор упрощённых версий программы. Эти алгоритмы были реализованы в инструменте статической верификации программ CPAchecker. Наши эксперименты показали, что предложенный метод может быть использован для нахождения ошибок в программных системах, используемых на практике.

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

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

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

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

Телекоммуникационные системы являются одними из самых трудоёмких видов ПО, вовлекая большое количество людей, денежных средств, а также времени. Декларативные предметно-ориентированные языки (DSLs) могут существенно помочь в разработке таких систем, реализуя подходящие абстракции. Мы используем термин «декларативные», подразумевая, что программы на таком DSL предназначаются не для программирования исполняемой логики, а для описания данных (базы данных сетевого устройства, структуры данных целевого кода и т.д.) и задания некоторого модельного поведения устройств при возникновении определённых событий.   Таким образом, исполнение таких программ в целях отладки невозможно осуществить, сгенерировав и запустив конечный код, т.е. не удаётся использовать средства типа xtext, MPS. Между тем отладка таких спецификаций является востребованной задачей в виду объёмности спецификаций (десятки тысяч строк кода), а также большого числа точечных изменений, вносимых при copy/paste, в ходе разработки очередной телекоммуникационной системы, принадлежащей данному семейству продуктов.

В предлагаемой статье описывается отладчик для предметно-ориентированного декларативного языка DevM. Этот язык предназначается для описания базы данных аппаратуры роутеров и свичей, задания специфической информации, необходимой для инициализации драйверов устройств, и описания высокоуровневого поведения системы при получении специфических событий из сети и от аппаратуры самого устройства. Язык ориентирован на использование в контексте семейства телекоммуникационных систем одной крупной телекоммуникационной компании. В рамках работы над отладчиком была уточнена исполняемая семантика DevM для задания событийно-ориентированного поведения системы, а также введена специальная модель (т.е. создана новая часть языка DevM) для задания отладочной конфигурации отлаживаемой системы. Исполнение программы на DevM выполняется без генерации целевого кода. Для наглядного отображения шага исполнения программы использовалась графическая событийно-ориентированная нотация. Интеграция созданного отладчика с DevM-фреймворком была выполнена с помощью Debug Adapter Protocol и языкового сервера DevM (language server), разработанного с помощью стека технологий Eclipse xText/EMF.

В средах системного программного обеспечения циркулирует огромное количество информации, поэтому крайне важно использовать эту информацию для улучшения их работы. Одной из таких систем является ядро Linux, которое не только поставляется с полностью открытым исходным кодом, но и предоставляет исчерпывающую историю о разработке в своем git-репозитории. Здесь каждое логическое изменение кода сопровождается сообщением, написанным разработчиком на естественном языке. Обрабатывая данные репозитория, мы сосредотачиваемся на коммитах с сообщениями об исправлении ошибок, поскольку анализ их текста может помочь выявить наиболее распространенные типы ошибок. Основываясь на наших предыдущих работах, в этой статье мы предлагаем использовать методы анализа данных. Для достижения наших целей мы предлагаем различные методы обработки сообщений в git-репозиториях и используем автоматизированные методы для выявления распространенных ошибок в них. Вычисляя расстояния между сообщениями об исправлении ошибок, превращая их в вектора и группируя в кластеры, мы далее можем эффективно классифицировать и выявлять наиболее часто возникающие ошибки. Наш подход применяется к нескольким важным частям ядра Linux, что позволяет понять, что происходит с ошибками в различных его подсистемах. В результате мы показываем сводку исправлений ошибок в таких частях ядра Linux, как kernel, sched, mm, net, irq, x86 и Arm64.