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

Процесс-ориентированное программирование — это подход к разработке управляющего программного обеспечения, при котором программа представляется в виде набора взаимодействующих процессов. PoST представляет собой процесс-ориентированное расширение языка ST из стандарта IEC 61131-3. Поскольку к управляющим системам часто предъявляются высокие требования надёжности, важную роль играет формальная верификация используемого в них программного обеспечения. Один из методов формальной верификации — дедуктивная верификация, которая включает построение формальной спецификации, генерацию условий корректности и их доказательство. Для доказательства мы применяем систему доказательства теорем Isabelle/HOL. При этом полностью автоматизирована только генерация условий корректности. Дедуктивная верификация сама по себе трудоёмка, поэтому её желательно автоматизировать в максимально возможной степени. Для управляющего программного обеспечения характерно наличие темпоральных требований, которые при дедуктивной верификации процесс-ориентированных программ задаются в виде инвариантов цикла управления. Однако этих требований часто оказывается недостаточно как инвариантов, что требует введения дополнительных инвариантов, содержащих вспомогательную информацию о программе. Ранее был предложен подход к доказательству условий корректности, в котором требования и дополнительные инварианты задаются с помощью шаблонов, а для доказательства условий корректности используются связанные с шаблонами леммы, удовлетворяющие предопределённым схемам. В данной статье рассматривается автоматизация доказательства как условий корректности, так и самих лемм, используемых для их доказательства. Описан ранее предложенный подход к автоматизации дедуктивной верификации и даётся введение в Isabelle/HOL. Представлены скорректированные схемы шаблонов и лемм, а также алгоритм порождения доказательств для лемм. Рассмотрена реализация этого алгоритма и ранее разработанного алгоритма генерации доказательств условий корректности. Предложенный подход демонстрируется на примере. Также приводится обзор связанных работ.

Декларативные модели процессов широко используются в process mining для гибкого описания поведения процессов с помощью наборов ограничений. Однако модели, автоматически извлекаемые из журналов событий, могут содержать несогласованные ограничения, что затрудняет их интерпретацию и делает их непригодными для исполнения, проверки соответствия или дальнейшего анализа. Существующие методы анализа согласованности либо опираются на автоматные конструкции с высокой асимптотической сложностью в худшем случае, либо используют эвристики, ориентированные на минимальные несогласованные подмножества (MIS), которые не дают полного формального описания обнаруживаемых ими паттернов несогласованности. В данной работе предлагается графовый подход к анализу несогласованности для ограниченного фрагмента языка Declare. Мы представляем зависимости между ограничениями с помощью графа следования задач и характеризуем несогласованность посредством трёх типов структурных свидетелей. На основе этого описания мы сначала выявляем кандидаты в несогласованные подмножества, а затем проверяем, является ли кандидат минимальным несогласованным подмножеством, с помощью специализированных процедур верификации. В отличие от подходов, основанных на автоматах, предлагаемый метод избегает явного построения произведений автоматов и вместо этого опирается на графовый анализ и конструктивное построение трасс. Мы реализовали предложенный подход и провели его экспериментальную оценку на реальных журналах событий, показав, что он практически применим и обеспечивает конкурентоспособное время работы.

В статье решается задача математического моделирования прямоугольного шума в электромагнитных сигналах, в частности на вихретоковых дефектограммах, для генерации качественных синтетических выборок при обучении алгоритмов машинного обучения для обнаружения и подавления прямоугольного шума в данных. Проведено комплексное исследование наивных моделей: детерминированного прямоугольного сигнала, прямоугольного сигнала с белым шумом и телеграфного процесса с белым шумом. Центральным объектом исследования является модель телеграфного процесса с белым шумом. Для этой модели аналитически выведены стационарные характеристики: функция плотности предельного распределения и автокорреляционная функция. Для оценки параметров модели впервые предложен и реализован полностью байесовский подход, использующий сэмплирование по Гиббсу и алгоритм прямой фильтрации и обратного сэмплирования (FFBS) для эффективного маргинализирования скрытых марковских состояний. Алгоритм быстро сходится, и к 1500-й итерации сэмплирования общая дисперсия параметров падает до значения $1e{-}6$. Установлено, что классические модели обладают фундаментальными ограничениями из-за несоответствующего реальности допущения о строгом постоянстве периода и скважности. Показано, что телеграфный процесс решает проблему стохастичности длительностей импульсов, однако игнорирование непрерывности переходных фронтов приводит к математическому артефакту — смещению мод теоретического предельного распределения по сравнению с эмпирическим. Также продемонстрировано, что отсутствие механизма низкочастотной фильтрации лишает автокорреляционную функцию модели характерной осциллирующей компоненты. Экспериментальное подтверждение значимости этих факторов обосновывает направление для дальнейших исследований — разработку модифицированных стохастических моделей, интегрирующих механизмы плавного переключения состояний для адекватного имитационного моделирования прямоугольного шума. В качестве эмпирической базы для тестирования моделей выступали вихретоковые дефектограммы рельсов. Тем не менее, разработанный математический аппарат может успешно использоваться для моделирования прямоугольного шума в других видах электромагнитных сигналах, например в ЭКГ и в магнитотеллурическом зондировании.

В статье рассматривается проблема оценки надёжности привязной высотной беспилотной телекоммуникационной платформы с использованием метода анализа дерева рисков. Целью работы является разработка и апробация методики, позволяющей количественно оценивать вероятность возникновения рисковых ситуаций и связанный с ними материальный ущерб при длительной эксплуатации платформы. В качестве результирующего рискового события рассмотрен сбой в обеспечении широкополосной беспроводной связи, выполняемой платформой. Представлено подробное техническое описание привязной платформы «Альбатрос», послужившее основой для выделения рисковых событий. Изложена общая теория и методология построения и анализа дерева рисков, включая оснащение модели вероятностными и стоимостными параметрами. На примере привязной высотной беспилотной телекоммуникационной платформы реализовано комплексное численное исследование, в рамках которого проведён анализ чувствительности ключевых выходных показателей (функции надёжности, квантилей, среднего времени до отказа, ожидаемого ущерба) к статистическим свойствам времени наступления отказов — коэффициенту вариации и типу распределения. Практические выводы, полученные по результатам исследования, показывают, что использование адекватных вероятностных моделей (в отличие от упрощённых экспоненциальных) критически важно для получения реалистичных прогнозов; выявлены наиболее опасные сценарии развития рисковых ситуаций и количественно оценён вклад факторов, влияющих на наступление этих событий. Предложенная методология является универсальной и может быть применена к широкому кругу сложных технических систем, в том числе другим привязным платформам, архитектура которых допускает декомпозицию на ключевые компоненты с установлением логических связей между их отказами. Полученные результаты могут быть использованы для обоснованного проектирования таких систем, планирования регламентных работ и оптимизации стратегий технического обслуживания.

Рассматривается динамика больших непериодических цепочек с адвективными связями между элементами. Основное предположение состоит в том, что количество $N$ элементов цепочки достаточно велико, поэтому естественным образом возникает малый параметр $\varepsilon=N^{-1}.$ Это предположение дает возможность от системы $N$ уравнений с запаздыванием перейти к исследованию пространственно-распределенного интегро-дифференциального уравнения, содержащего малый параметр и использовать асимптотические методы для исследования динамических свойств этого уравнения. Связи между элементами цепочек являются разностной аппроксимацией оператора адвекции (переноса), поэтому их называют адвективными. Еще одно предположение состоит в том, что цепочки не являются кольцевыми, т.е. краевые условия для рассматриваемых систем не обладают свойствами периодичности. Рассматриваются неклассические краевые условия, которые способствуют появлению новых динамических эффектов. Выделены критические случаи в задаче об устойчивости состояния равновесия и показано, что они имеют бесконечную размерность в том смысле, что бесконечно много корней характеристического уравнения стремятся к мнимой оси при стремлении к нулю малого параметра. В этой ситуации известные методы исследования, основанные на использовании инвариантных интегральных многообразий и нормальных форм, непосредственно не применимы. Используются методы квазинормальных форм, нелокальная динамика которых определяет локальное поведение решений рассматриваемых цепочек. Основные результаты состоят в построении квазинормальных форм с помощью специальных асимптотических методов. Это дает возможность получить главные приближения по параметру $\varepsilon$ решений исходной цепочки.

В статье рассматривается задача ранжирования планов выполнения SQL-запросов по времени выполнения. Такая задача представляет интерес для интеллектуальной оптимизации запросов, поскольку позволяет оценить, насколько выбранное описание плана сохраняет информацию, связанную с фактической стоимостью его исполнения. Предлагается метод, в котором вместо структурной кодировки дерева плана используется его текстовое описание, для которого затем строится векторное представление с помощью модели векторных представлений. Поверх полученного векторного представления обучается компактная предсказательная модель, используемая для ранжирования планов. В работе сравниваются три подхода: предсказательная модель из подхода Bao, использующая структурную кодировку дерева плана, стоимостная оценка оптимизатора PostgreSQL и предложенный метод на основе текстового описания плана и моделей векторных представлений. Дополнительно исследуются несколько моделей векторных представлений и два варианта текстового описания плана — исходный текст и нормализованное описание. Эксперименты проведены на наборе CEB, построенном на данных IMDb, в двух режимах тестирования: при случайном разбиении и при разбиении по шаблонам запросов. Качество оценивалось по попарной точности и коэффициенту Спирмена. Показано, что при случайном разбиении выборки лучшая конфигурация на основе модели jina-code-embeddings-0.5b превосходит модель Bao и стоимостную оценку оптимизатора по обеим метрикам ранжирования. Установлено также, что исходное текстовое описание плана для всех рассмотренных моделей оказывается более информативным, чем использованная схема нормализации. При разбиении выборки по шаблонам запросов качество всех обучаемых подходов снижается; при этом лучшая модель на основе векторных представлений и модель Bao остаются на сопоставимом уровне между собой, однако по обеим метрикам уступают стоимостной оценке оптимизатора. Полученные результаты показывают, что текстовое описание плана и модели векторных представлений могут использоваться как основа для построения предсказательных моделей ранжирования, хотя проблема устойчивой генерализации на ранее не наблюдавшиеся шаблоны запросов остаётся открытой.