№ 4 (2025)

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

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

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

В условиях развития современной экономики быстрыми темпами расширяется сфера применения Больших Данных (базы данных, производительные вычисления, скоростные каналы сети) и автоматизированных методов работы в данной сфере (проектирование данных систем, управление ими и мониторинг). Особую популярность приобретают системы Искусственного Интеллекта как методы автоматизации всех вышеперечисленных моментов. В нашей стране решаются серьезные задачи в этих областях компьютерных наук. Несмотря на ряд системных проблем, происходит формирование распределенной сети Суперкомпьютерных Центров Коллективного пользования, которая призвана решить задачу рационального использования суперкомпьютерных систем. Также существуют успехи в рамках работ по созданию технологий написания и трансляции параллельного Программного Обеспечения. В статье приведена краткая справка о программных решениях, используемых в Операционной Системе Plan 9. В частности, рассмотрен сетевой протокол файловой системы 9P и приведено его краткое сравнение с NFS (на данный момент). На основе этого протокола автором предложена программная архитектура Общего Скоростного Буфера Памяти для промежуточных вычислений, необходимого в оптимизации численных методов и машинного обучения внутри распределенных вычислительных систем. Автор предлагает использовать возможности протокола для организации мониторинга удаленных хостов, а также управления процессами и устройствами на нем. В статье намечены задачи по усовершенствованию сетевого протокола 9P. Сделаны некоторые замечания об особенностях применения протокола в его современном виде. Сделан вывод о большом потенциале применения технологий на его основе.

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

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

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