Данная статья посвящена разработке процедуры автоматизированной миграции Java-программ на новый набор библиотек. Задача миграции (портирования) кода часто встречается в современных программных проектах. Например, такая задача может возникнуть, когда проект необходимо перенести на более безопасную или функциональную библиотеку, на новую платформу или на новую версию уже используемой в проекте библиотеки. В данной работе представлена процедура автоматизированной миграции, основанная на семантическом подходе. Для процедуры миграции была разработана метамодель библиотеки, использующая предложенный ранее авторами формализм и предназначенная для описания библиотек на объектно-ориентированных языках. Формализм описывает поведение библиотек с помощью системы расширенных конечных автоматов (РКА). Процедура миграции разбита на пять шагов, каждый шаг подробно описан в тексте статьи. В процедуре используется алгоритм вычисления эквивалентной трассы на основе поиска в ширину, расширенный для решения задач миграции. Предложенная процедура реализована в прототипе инструмента миграции. Инструмент включает в себя модули извлечения трассы выполнения программ, визуализации моделей библиотек, взаимодействия с пользователем и непосредственно миграции. Для инструмента был разработан язык описания библиотек. Прототип инструмента был протестирован как на искусственных примерах, так и на существующем проекте. В статье подробно описаны проведенные эксперименты, отдельно отмечены сложности, возникающие в процессе миграции тестовых примеров, и то, как они решаются в предложенной процедуре. В качестве библиотек в экспериментах используются реализации протокола HTTP и библиотеки протоколирования. Результаты тестирования показали, что миграция кода может быть успешно автоматизирована с использованием разработанной процедуры.

Система обозначений диаграмм состояний (state machines) широко применяется в качестве формального средства описания поведения систем. Обычно для одной и той же программной системы можно создать много разных диаграмм состояний. Некоторые из этих моделей могут оказаться эквивалентными, но во многих случаях разные диаграммы состояний описывают одну и ту же систему на разных уровнях абстракции. В этой статье мы предлагаем подход, позволяющий провести фактическое измерение уровня абстракции диаграмм состояний по отношению к заданной реализации программной системы. Диаграмма состояний считается тем менее абстрактной, чем ближе она концептуально к реализованной системе. Согласно нашему подходу эта отдаленность диаграммы состояний от реализации системы измеряется путем применения критерия покрытия, используемого для тестирования мутации программного обеспечения. Уровень абстракции диаграмм состояний можно рассматривать как новый вид метрики. Что касается других метрик, то знание значения уровня абстракции заданной диаграммы состояний дает возможность оценить ее качество в числовых терминах. В тех проектах по разработке программного обеспечения, которые начинаются с построения модели, метрика абстракции может помочь избежать деградации моделей, поскольку она позволяет измерить фактическое отдаление спецификации поведения системы, представленной в виде диаграммы состояний, от текущей реализации системы. В отличие от прочих метрик для диаграмм состояний уровень абстракции нельзя вычислить статически, основываясь лишь на структуре самой диаграммы; для этого нужно сравнивать выполнения диаграмм состояний и соответствующую реализацию системы. Статья публикуется в авторской редакции.

Статическая верификация исходного кода программы является важным элементом надежности программного обеспечения. Под верификацией предполагается доказательство соответствия поведения программы ее спецификации. Во многих языках программирования используется как статическая, так и динамическая проверка типов. Таким образом, статический тайп-чекер старается проверить все возможное во время компиляции, а динамический проверяет оставшееся. На данный момент язык программирования Jolie имеет динамическую систему типов, что позволяет обнаруживать ошибки только во время выполнения программы. Статическая система типов для языка была формально определена на бумаге, но пока не реализована. В этой статье мы представим прототип статического тайп-чекера для языка программирования Jolie (JolieStaticTypeChecker или JSTC), основанный на SMT-решателе. Мы опишем базовую теорию, необходимую для реализации тайп-чекера, саму реализацию, а также процесс статического анализа программы. Статья публикуется в авторской редакции.

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

разыменование нулевого указателя; безопасность нулевых ссылок; безопасность пустых ссылок; инициализация объектов; статический анализ; эталонные тесты безопасности нулевых ссылок

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

Данная работа представляет дальнейшее развитие метода верификации финитной итерации [7]. Он расширяет метод смешанной аксиоматической семантики [1], предложенный для верификации C-light программ. Это расширение включает метод верификации для финитной итерации над неизменяемыми массивами с выходом из цикла в C-light программах. Метод содержит правило вывода для итерации без инвариантов, которое использует специальную функцию, выражающую действие тела цикла. Данное правило было реализовано в генераторе условий корректности, являющемся частью нашей системы верификации C-light программ. Для доказательства порождённых условий корректности применяется метод математической индукции, вызывающий сложности у SMT-решателей. В нашей системе верификации на стадии доказательства используется SMT-решатель CVC4. Для преодоления упомянутой трудности применяется стратегия переписывания условий корректности. Для доказательства условий корректности предложен метод, основанный на расширении теории новыми теоремами. Рассмотрен пример, иллюстрирующий применение данных методов. Статья публикуется в авторской редакции.

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

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

Цель данной статьи — проанализировать, насколько эффективно могут применяться различные типы тезаурусных связей в задачах классификации текстов. Основой исследования является автоматически сгенерированный тезаурус предметной области, содержащий три типа связей: синонимические, иерархические и ассоциативные. Для генерации тезауруса используется гибридный метод, основанный на нескольких лингвистических и статистических алгоритмах выделения семантических связей и позволяющий создать тезаурус с достаточно большим числом терминов и связей между ними. Авторы рассматривают две задачи: тематическая классификация текстов и классификация больших новостных статей по тональности. Для решения каждой из них авторами были использованы два подхода, каждый из которых дополняет стандартные алгоритмы процедурой, применяющей связи тезауруса для определения семантических особенностей текстов. Подход к тематической классификации включает в себя стандартный алгоритм BM25 вида «обучение без учителя» и процедуру, использующую синонимические и иерархические связи тезауруса предметной области. Подход к классификации по тональности состоит из двух шагов. На первом шаге создается тезаурус, тональные веса терминов которого считаются в зависимости от частоты встречаемости в обучаемой выборке или от веса соседей по тезаурусу. На втором шаге тезаурус применяется для вычисления признаков слов из текстов и классификации текстов методом опорных векторов или наивным байесовским классификатором. В экспериментах с корпусами BBCSport, Reuters, PubMed и корпусом статей об американских иммигрантах авторы варьировали типы связей, которые участвуют в классификации, и степень их использования. Результаты экспериментов позволяют оценить эффективность применения тезаурусных связей для классификации текстов на естественном языке и определить, при каких условиях те или иные связи имеют большую значимость. В частности, наиболее полезными тезаурусными связями оказались синонимические и иерархические, так как они обеспечивает лучшее качество классификации.

В статье вводится определение неориентированного кратного графа произвольной натуральной кратности k > 1. Кратный граф содержит ребра трех типов: обычные, кратные и мультиребра. Ребра последних двух типов представляют собой объединение k связанных ребер, которые соединяют 2 или k + 1 вершину соответственно. Связанные ребра могут использоваться только согласованно. Если вершина инцидентна какому-либо кратному ребру, то она может быть инцидентна другим кратным ребрам, а также она может быть общим концом k связанных ребер какого-либо мультиребра. Если вершина является общим концом какого-либо мультиребра, то она не может быть общим концом никакого другого мультиребра. Отдельно рассматривается класс делимых кратных графов, основной особенностью которых является возможность выделения k частей, согласованных на всех связанных ребрах и не содержащих общих ребер. Каждая из частей является обычным графом. Для кратного графа обобщаются понятия степени вершины, связности графа, пути, цикла, веса ребра и длины пути. Вводится понятие множества достижимости по обычным и по кратным ребрам, определяется свойство смежности двух множеств достижимости. Показано, что проверка связности кратного графа может быть выполнена за полиномиальное время с помощью алгоритма, основанного на поиске множеств достижимости и проверки их смежности. Рассматривается критерий существования кратного пути между двумя вершинами и ставится задача о кратчайшем кратном пути. Строится алгоритм поиска кратчайшего пути в кратном графе, который использует алгоритм Дейкстры для поиска кратчайших путей в подграфах, соответствующих отдельным множествам достижимости.

В работе для одного класса слабо нелинейных систем с зависящими от состояния коэффициентами рассматривается подход к построению нелинейного следящего управления по выходу на конечном интервале времени. Предложенный метод синтеза состоит из двух основных этапов. Сначала с помощью ранее предложенного автором алгоритма на основе уравнений Риккати, с зависящими от состояния коэффициентами (State Dependent Riccati Equation – SDRE), находится нелинейный регулятор по состоянию. На втором этапе ставится задача построения наблюдателя полного порядка, которая сводится к задаче дифференциальной игры. Вид её решения получен с помощью принципа гарантированного управления, позволяющего относительно заданного функционала найти наилучшие коэффициенты наблюдателя при наихудшей реализации неопределенностей. Однотипность полученных уравнений позволила для определения матрицы наблюдателя использовать алгоритм решения из первого этапа. Особенностями предложенного подхода являются отсутствие принципа разделения задач синтеза управления и наблюдения, который имеет место в линейных системах, поскольку матрица коэффициентов наблюдателя оказалась зависимой от матрицы коэффициентов обратной связи, и использование численно-аналитических процедур для определения этих матриц, что позволяет значительно снизить вычислительную сложность алгоритма управления.

Представлено краткое изложение доклада авторов на семинаре “Моделирование и анализ информационных систем”, Ярославль, 17 мая 2017 г. В нём рассматривается взаимосвязь задач по автоматизации построения тезауруса и спецификации текста стихотворного произведения в поэтологии.