Математические модели распределенных вычислений, построенные на основе исчисления мобильных процессов (\(π\)-исчисления), широко используются для проверки свойств информационной безопасности криптографических протоколов. Поскольку \(π\)-исчисление является полной по Тьюрингу моделью вычислений, эта задача в общем случае алгоритмически неразрешима. Поэтому ее исследование проводится лишь для некоторых специальных классов процессов \(π\)-исчисления с ограниченными вычислительными возможностями, например, для нерекурсивных процессов, в которых все вычисления имеют ограниченную длину, для процессов с ограниченным числом параллельных компонентов и др. Однако и в этих случаях предложенные разрешающие алгоритмы оказываются весьма трудоемкими. Мы полагаем, что это обусловлено самой природой процессов \(π\)-исчисления. Цель данной работы — показать, что даже для наиболее слабой модели пассивного противника и для сравнительно простых протоколов, в которых используются лишь базовые операции \(π\)-исчисления, задача проверки свойств информационной безопасности этих протоколов является co-NP-полной.

В статье представлена онтология процессов, близких взаимодействующим последовательным процессам Хоара. Она является частью интеллектуальной системы поддержки верификации свойств поведения таких процессов. Наше онтологическое представление процессов ориентировано как на применение формальных методов верификации, так и на извлечение информации из технической документации (с помощью нашей ранее разработанной системы извлечения информации из текстов на естественном языке). Мы описываем классы и домены онтологии, которые определяют взаимодействующие процессы. Эти процессы характеризуются множествами локальных и разделяемых переменных, списком действий над этими переменными, которые изменяют их значения, списком каналов взаимодействия процессов (которые, в свою очередь, характеризуются типом чтения сообщений, емкостью, способами записи и считывания, а также надежностью), списком коммуникационных действий для отправки сообщений. Помимо формального математического определения классов и доменов онтологии, приведены примеры описаний некоторых онтологических классов, а также типовых свойств и аксиом для них в редакторе Prot ́eg ́e на языке OWL с использованием правил вывода на языке SWRL. Для онтологического представления взаимодействующих процессов определяется их формальная операционная семантика, которая задается с использованием помеченной системы переходов. В интерливинговой модели она сводится к локальной операционной семантике отдельных экземпляров процессов. Представлена специализация онтологии для некоторых типов процессов из предметной области систем автоматического управления, моделирующих типовые функциональные элементы системы автоматического управления (датчики, сравнивающие устройства и регулирующие устройства), а также их комбинации. Понятия специализированной онтологии иллюстрируются на примере управляющей части системы розлива бутылок.

Формальные языки моделирования играют важную роль в разработке программного обеспечения, так как позволяют пользователям, во-первых, определять функциональные требования, которые также служат документацией для проекта, а во-вторых, доказывать корректность свойств систем, что особенно важно для критических систем. Однако не существует четкого понимания того, как сопоставить формальную модель и определенный язык программирования. В качестве решения данной проблемы авторы статьи предлагают использовать возможность source-to-source соответствия между моделями, описанными на языке Event-B (языке моделирования для реактивных приложений и систем), и программами на объектно-ориентированном языке программирования Eiffel. Предложенное решение не только автоматически генерирует соответствующий модели на Event-B код на Eiffel, но также переводит свойства модели в виде контрактов. Контракты соответствуют принципу Design-by-Contract и нативно поддерживаются в Eiffel. Реализация решения доступна как плагин EB2Eiffel в Rodin (среде разработки для Event-B). Таким образом, пользователи могут разрабатывать различные системы, начиная с моделирования функциональных требований (свойств) в Event-B, затем формально доказывая корректность этих свойств в Rodin и, наконец, используя EB2Eiffel для перевода модели на язык программирования. Используя Eiffel, пользователи могут расширять и модифицировать реализацию модели и доказывать корректность измененной модели относительно ее оригинальной, изначально переведенной версии. Также в статье описан процесс тестирования EB2Eiffel разными моделями, написанными на Event-B, и представлены ограничения плагина. Статья публикуется в авторской редакции.

Цель проекта “Платформенно-независимый подход к формальной спецификации и верификации стандартных математических функций” --- инкрементальный комбинированный подход к спецификации и верификации стандартных математических функций, таких как sqrt, cos, sin и так далее. Платформенно-независимый подход предполагает простую аксиоматизацию машинной арифметики в терминах вещественной арифметики (то есть арифметики поля \(\mathbb{R}\) вещественных чисел), не фиксируя ни основание системы счисления, ни формат машинного слова.
Инкрементальность означает, что спецификация и верификация начинается с рассмотрения наиболее “простого” случая – элементарной спецификации и верификации простого алгоритма, работающего с вещественными числами, а заканчивается модификацией элементарной спецификации и алгоритма для машинной арифметики и верификацией алгоритма, работающего в машинной арифметике. А комбинированность подхода означает, что мы начинаем с рассмотрения “базового случая” --- “ручной” верификации (с ручкой и бумагой) для алгоритма, работающего в вещественной арифметике, затем выполняем ручную верификацию алгоритма, работающего в машинной арифметике, используя верификацию для базового случая в качестве “конспекта” (proof-outlines), а заканчиваем --- верификацией с использованием автоматизированной системы построения/поиска доказательства для того, чтобы исключить апелляцию к “очевидности” в ручной верификации. В статье платформенно-независимый инкрементальный комбинированный подход применяется для спецификации и верификации стандартной математической функции квадратного корня. В настоящий момент автоматизированная верификация разработанных алгоритмов выполнена только частично: с использованием системы ACL2 доказана реализуемость (существование) чисел с фиксированной запятой и таблицы начальных приближений квадратного корня.

Для обеспечения безопасности движения на железнодорожном транспорте регулярно проводится неразрушающий контроль рельсов с применением различных подходов и методов, включая методы магнитной и вихретоковой дефектоскопии. Актуальной задачей является автоматический анализ больших массивов данных (дефектограмм), которые поступают от соответствующего оборудования. Под анализом понимается процесс определения по дефектограммам наличия дефектных участков наряду с выявлением конструктивных элементов рельсового пути. Данная статья посвящена задаче распознавания образов конструктивных элементов железнодорожных рельсов по дефектограммам многоканальных магнитных и вихретоковых дефектоскопов. Рассматриваются три класса конструктивных элементов рельсового пути: 1) болтовой стык с прямым или скошенным соединением рельсов, 2) электроконтактная сварка рельсов и 3) алюмотермитная сварка рельсов. Образы, которые не могут быть отнесены к этим трем классам, условно считаются дефектами и выносятся в отдельный четвертый класс. Для распознавания образов конструктивных элементов на дефектограммах применяется нейронная сеть, реализованная в рамках открытой библиотеки TensorFlow. С этой целью каждая выделенная для анализа область дефектограммы преобразуется в графический образ в градации серого цвета размером 20 на 39 пикселей.

Пусть \(C\) --- выпуклое тело, \(S\) невырожденный симплекс в \({\mathbb R}^n\). Через \(\tau S\) обозначим образ \(S\) при гомотетии относительно центра тяжести \(S\) с коэффициентом \(\tau\). Под \(\xi(C;S)\) понимается минимальное \(\tau>0,\) для которого \(C\) является подмножеством симплекса \(\tau S\). По определению, \(\alpha(C;S)\) есть минимальное \(\tau>0\), такое что \(C\) принадлежит трансляту симплекса \(\tau S\). Ранее автор доказал, что справедливы равенства \(\xi(C;S)=(n+1)\max\limits_{1\leq j\leq n+1} \max\limits_{x\in C}(-\lambda_j(x))+1\) (если \(C\not\subset S\)), \(\alpha(C;S)= \sum\limits_{j=1}^{n+1} \max\limits_{x\in C} (-\lambda_j(x))+1.\) Здесь \(\lambda_j\) --- линейные функции, называемые базисными многочленами Лагранжа симплекса \(S\). Они таковы, что числа \(\lambda_j(x),\ldots, \lambda_{n+1}(x)\) являются барицентрическими координатами точки \(x\in{\mathbb R}^n\). В предыдущих работах автора указанные формулы исследовались в ситуации, когда \(C\) представляет собой \(n\)-мерный единичный куб \(Q_n=[0,1]^n\). В статье рассматривается случай, когда \(C\) есть единичный евклидов шар \(B_n=\{x: \|x\|\leq 1\},\) где \(\|x\|=\left(\sum\limits_{i=1}^n x_i^2 \right)^{1/2}.\) Устанавливаются различные соотношения для \(\xi(B_n;S)\) и~\(\alpha(B_n;S)\), а также приводится их геометрическая интерпретация. Например, если \(\lambda_j(x)= l_{1j}x_1+\ldots+ l_{nj}x_n+l_{n+1,j},\) то \(\alpha(B_n;S)= \sum\limits_{j=1}^{n+1}\left(\sum\limits_{i=1}^n l_{ij}^2\right)^{1/2}\). Минимальное возможное значение каждой из величин \(\xi(B_n;S)\), \(\alpha(B_n;S)\) для \(S\subset B_n\) равно \(n\) и соответствует правильному симплексу, вписанному в \(B_n\). Даётся сравнение с результатами, полученными ранее для \(C=Q_n\).

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

Поиск редакционного расстояния между графовыми моделями (определение схожести графовых моделей) является важной задачей в различных областях компьютерных наук, таких как анализ изображений, машинное обучение, химическая информатика. В последнее время, в связи с развитием методов извлечения и анализа процессов, появилась необходимость в адаптации существующих методов сравнения графовых моделей для анализа моделей процессов (аннотированных графов), извлекаемых из логов событий информационных систем. Методы нахождения минимального редакционного расстояния между графами могут быть использованы для обнаружения шаблонов (подпроцессов), а также для сравнения извлекаемых моделей процессов. Как было показано экспериментально и теоретически обосновано, точные методы нахождения минимального редакционного расстояния между извлекаемыми моделями процессов (и графами в общем случае) имеют большую временную сложность и могут быть применены лишь к небольшим моделям процессов. В этой статье мы оцениваем точность и временные характеристики генетического алгоритма, применяемого для нахождения расстояний между моделями процессов, извлекаемых из логов событий. В частности мы находим расстояния между BPMN (Business Process Model and Notation) моделями, извлекаемыми из логов событий с помощью различных алгоритмов синтеза. В этой работе показано, что представленный генетический алгоритм позволяет в значительной степени уменьшить время вычислений, при этом показывая результаты, близкие к оптимальным (минимальным редакционным расстояниям).

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