Журнал программирование архив номеров

О научном журнале«Программирование»

Журнал основан в 1975 году и публикует статьи по всем проблемам, связанным с теоретическим и практическим программированием: операционные системы, технологии программирования, языки программирования и компиляторы, параллельное программирование, верификация и тестирование программ, машинная графика, компьютерная алгебра и т.п. Журнал предназначен для исследователей, практиков и студентов. Периодичность выпуска – 6 номеров в год. Журнал внесен в список ВАК.

Архив научных статейиз журнала «Программирование»

• АВТОМАТИЗАЦИЯ СОЗДАНИЯ ТАБЛИЦЫ КОНФИГУРАЦИИ ПРОГРАММНОГО ОБЕСПЕЧЕНИЯ ДЛЯ СИСТЕМ РЕАЛЬНОГО ВРЕМЕНИ В АВИОНИКЕ

  БАТОВА С.В., БЛАГОНРАВОВ С.А., ЖАРИНОВ И.О., КОНОВАЛОВ П.В., УТКИН С.Б. — 2015 г.

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

• АВТОРСКИЙ УКАЗАТЕЛЬ СТАТЕЙ, ОПУБЛИКОВАННЫХ В 2014 ГОДУ

  2015

• АЛГОРИТМ ПРОВЕРКИ ТРИВИАЛЬНОСТИ «СМЕШАННЫХ» ИДЕАЛОВ В КОЛЬЦЕ ДИФФЕРЕНЦИАЛЬНЫХ МНОГОЧЛЕНОВ

  ЗОБНИН А.И., ЛИМОНОВ М.А. — 2015 г.

  В статье предлагается алгоритм проверки тривиальности идеала [f] + (h 1,…., h t) в обыкновенном кольце дифференциальных многочленов при некотором дополнительном условии на многочлен f. Эта задача тесно связана, с одной стороны, с задачей Колчина об экспонентах дифференциальных идеалов, а с другой — с вопросами конечности дифференциальных стандартных базисов.

• АЛГОРИТМИЧЕСКИЕ ВОПРОСЫ КОНЪЮНКТИВНОЙ ДЕКОМПОЗИЦИИ БУЛЕВЫХ ФОРМУЛ

  ЕМЕЛЬЯНОВ П.Г., ПОНОМАРЕВ Д.К. — 2015 г.

  Под конъюнктивной декомпозицией понимают отыскание двух или более формул, компонент декомпозиции, конъюнкция которых эквивалентна исходной формуле. Декомпозиция называется дизъюнктной, если множества переменных у компонент не пересекаются. В статье показано, что проблема существования дизъюнктной конъюнктивной декомпозиции является трудной для булевых формул, заданных в КНФ/ДНФ. Для позитивных ДНФ, СДНФ и АНФ показано существование полиномиального алгоритма для нахождения компонент дизъюнктной декомпозиции. Данный результат следует из эффективной факторизации полилинейных полиномов над конечным полем порядка 2, для которой в статье предложен алгоритм, основанный на тестировании равенства нулю частных производных полилинейных полиномов.

• АССОЦИИРОВАННЫЕ ТИПЫ И РАСПРОСТРАНЕНИЕ ОГРАНИЧЕНИЙ НА ПАРАМЕТРЫ-ТИПЫ ДЛЯ ОБОБЩЁННОГО ПРОГРАММИРОВАНИЯ НА SCALA

  ПЕЛЕНИЦЫН А.М. — 2015 г.

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

• ВЫСОКОУРОВНЕВАЯ МОДЕЛЬ ПАМЯТИ ПРОМЕЖУТОЧНОГО ЯЗЫКА JESSIE С ПОДДЕРЖКОЙ ПРОИЗВОЛЬНОГО ПРИВЕДЕНИЯ ТИПОВ УКАЗАТЕЛЕЙ

  МАНДРЫКИН М.У., ХОРОШИЛОВ А.В. — 2015 г.

  В статье представлен промежуточный язык, предназначенный для использования в качестве целевого анализируемого языка при верификации промышленного кода на языке GNU С (в частности, модулей ядра Linux). Язык представляет собой расширение существующего промежуточного языка, используемого подключаемым модулем JESSIE в системе статического анализа Frama-C. Он имеет семантику, совместимую с семантикой языка Си (в частности, для массивов), изначально поддерживает различаемые объединения и префиксные (иерархические) приведения типов указателей на структуры, и расширен ограниченной поддержкой низкоуровневого приведения типов указателей. Подходы к трансляции исходного Си-кода в промежуточный язык, а также трансляции промежуточного языка во входной язык платформы дедуктивной верификации Why3 рассматриваются на примерах. Эти примеры иллюстрируют выразительность расширенного промежуточного языка и эффективность получаемых аксиоматических спецификаций.

• ДОКАЗАТЕЛЬСТВО СВОЙСТВ ФУНКЦИОНАЛЬНЫХ ПРОГРАММ МЕТОДОМ НАСЫЩЕНИЯ РАВЕНСТВАМИ

  ГРЕЧАНИК С.А. — 2015 г.

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

• ИССЛЕДОВАНИЕ ОДНОЙ ВЕЩЕСТВЕННОЙ АЛГЕБРАИЧЕСКОЙ ПОВЕРХНОСТИ

  БАХТИН А.Б., БРЮНО А.Д. — 2015 г.

  Дается описание некоторого вещественного алгебраического многообразия в R 3. Это многообразие играет важную роль в исследовании нормализованного потока Риччи на обобщенных пространствах Уоллаха. Для понимания структуры многообразия дается описание всех его особых точек. В силу наличия внутренней симметрии изучаемого объекта, часть исследования проводится с использованием элементарных симметрических многочленов. Все вычисления в препринте выполнены с использованием алгоритмов компьютерной алгебры, в частности, с использованием базисов Грёбнера и алгоритмов работы с полиномиальными идеалами. В качестве сопутствующего результата сформулировано и доказано утверждение о структуре дискриминантной поверхности кубического многочлена.

• КАЧЕСТВЕННОЕ ИССЛЕДОВАНИЕ МОДЕЛИ ГЕНА С ИСПОЛЬЗОВАНИЕМ АЛГОРИТМОВ КОМПЬЮТЕРНОЙ АЛГЕБРЫ

  БУЛЬЕ ФРАНСУА, ЛЁМЭР ФРАНСУА, РОМАНОВСКИЙ ВАЛЕРИЙ, ХАН МАОАН — 2015 г.

  С использованием алгоритмов и пакетов систем компьютерной алгебры проведено качественное исследование трехмерной автономной системы ОДУ, использованной в работе [1] для моделирования динамики гена. Предложен вычислительный подход, основанный на алгоритмах теории исключения, для нахождения инвариантных поверхностей многомерных полиномиальных систем дифференциальных уравнений, который позволяет свести изучение динамики системы к исследованию динамики траекторий системы меньшего порядка. Предложен также эффективный подход, основанный на использовании функций Ляпунова, для изучения бифуркаций Андронова-Хопфа, который использован для поиска таких бифуркаций в рассматриваемой модели.

• КОМПАКТНОЕ ПРЕДСТАВЛЕНИЕ ПОЛИНОМОВ ДЛЯ АЛГОРИТМОВ ВЫЧИСЛЕНИЯ БАЗИСОВ ГРЁБНЕРА И ИНВОЛЮТИВНЫХ БАЗИСОВ

  ЯНОВИЧ Д.А. — 2015 г.

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

• КОМПАРАТИВНАЯ ТРАССОВАЯ СЕМАНТИКА ВРЕМЕННЫХ СЕТЕЙ ПЕТРИ

  БУШИН Д.И., ВИРБИЦКАЙТЕ И.Б. — 2015 г.

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

• КОНФИГУРИРУЕМАЯ СИСТЕМА СТАТИЧЕСКОЙ ВЕРИФИКАЦИИ МОДУЛЕЙ ЯДРА ОПЕРАЦИОННЫХ СИСТЕМ

  ЗАХАРОВ И.С., МАНДРЫКИН М.У., МУТИЛИН В.С., НОВИКОВ Е.М., ПЕТРЕНКО А.К., ХОРОШИЛОВ А.В. — 2015 г.

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

• МОДЕЛИРОВАНИЕ КВАНТОВОГО АЛГОРИТМА ОПРЕДЕЛЕНИЯ ФАЗЫ

  ПРОКОПЕНЯ А.Н. — 2015 г.

  В статье обсуждается квантовый алгоритм оценки фазы, которая определяет собственное значение унитарного оператора. Предполагается, что собственный вектор оператора и соответствующая ему квантовая схема заданы. Регистр памяти, в который записывается приближеное значение фазы, содержит n кубитов, что позволяет определить фазу с точностью до 2 — n с вероятностью большей, чем 8/π 2. В качестве примера выполнены вычисления в случае квантового оператора сдвига фазы. Моделирование квантового алгоритма и вычисление собственного значения производится с помощью пакета “QuantumCircuit”, написанного на языке системы компьютерной алгебры Wolfram Mathematica, которая также используется для выполнения всех расчетов и визуализации полученных результатов.

• МОДЕЛИРОВАНИЕ ОКРУЖЕНИЯ С ИСПОЛЬЗОВАНИЕМ ШАБЛОНОВ ДЛЯ СТАТИЧЕСКОЙ ВЕРИФИКАЦИИ МОДУЛЕЙ ЯДРА LINUX

  ЗАХАРОВ И.С., МУТИЛИН В.С., ХОРОШИЛОВ А.В. — 2015 г.

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

• ОБРАТИМЫЕ ПРЕОБРАЗОВАНИЯ ДАРБУ ТИПА I

  ШЕМЯКОВА Е.С. — 2015 г.

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

• ПАРАЛЛЕЛЬНЫЕ ВЫЧИСЛЕНИЯ НА ГРАФЕ

  БУРДОНОВ И.Б., КОСАЧЕВ А.С., КУЛЯМИН В.В. — 2015 г.

  Рассматривается задача параллельного вычисления значения функции от мультимножества значений, записанных в вершинах ориентированного графа. Вычисление выполняется автоматами, находящимися в вершинах графа и обменивающихся между собой сообщениями, передаваемыми по дугам графа (в направлении их ориентации). Предполагается, что ёмкость дуги, то есть число одновременно передаваемых по ней сообщений, ограничена. Вычисление инициируется сообщением, приходящим извне в автомат выделенной начальной вершины графа. Этот же автомат в конце работы посылает вовне вычисленное значение функции. Для решения этой задачи предлагаются два алгоритма. Первый алгоритм выполняет исследование графа, основанное на его обходе. Его цель — разметить граф с помощью изменения состояний автоматов в вершинах. Строятся прямой и обратный остовы графа. Прямой остов ориентирован от корня, которым является начальная вершина графа. Обратный остов ориентирован к тому же корню. Кроме того, в каждой вершине устанавливается значение счётчика входящих дуг обратного остова. Такая разметка используется вторым алгоритмом, который и производит вычисление значения той или иной функции. Это вычисление основано на алгоритме пульсации: сначала от автомата начальной вершины по всему графу распространяются сообщения-вопросы, которые должны достигнуть каждой вершины, а затем от каждой вершины “в обратную сторону” к начальной вершине двигаются сообщения-ответы. Алгоритм пульсации, по сути, вычисляет агрегатные функции, для которых значение функции от объединения мультимножеств вычисляется по значениям функции от этих мультимножеств. Однако показано, что любая функция f (x) имеет агрегатное расширение, то есть может быть вычислена как h(f0(x)), где f’ — агрегатная функция. Заметим, что разметка графа не зависит от той функции, которая будет вычисляться. Это означает, что разметка графа выполняется один раз, после чего может многократно использоваться для вычисления различных функций.

• ПОИСК РАЦИОНАЛЬНЫХ РЕШЕНИЙ ДИФФЕРЕНЦИАЛЬНЫХ И РАЗНОСТНЫХ СИСТЕМ С ПОМОЩЬЮ ФОРМАЛЬНЫХ РЯДОВ

  АБРАМОВ С.А. — 2015 г.

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

• ПОПОЛНЕНИЕ ОНТОЛОГИЙ НА ОСНОВЕ АЛГЕБРАИЧЕСКОГО ФОРМАЛИЗМА ИНФОРМАЦИОННЫХ СИСТЕМ И МУЛЬТИАГЕНТНЫХ АЛГОРИТМОВ АНАЛИЗА ТЕКСТА

  ГАРАНИНА Н.О., СИДОРОВА Е.А. — 2015 г.

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

• ПРИМЕНЕНИЕ МЕТОДОВ ИНТЕЛЛЕКТУАЛЬНОГО АНАЛИЗА ТЕКСТОВОЙ ИНФОРМАЦИИ ДЛЯ ПРЕДОТВРАЩЕНИЯ УТЕЧЕК ДАННЫХ

  МАШЕЧКИН И.В., ПЕТРОВСКИЙ М.И., ЦАРЕВ Д.В. — 2015 г.

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

• РОГОВЫЕ СИСТЕМЫ ГОМОМОРФНОГО ШИФРОВАНИЯ И ЗАЩИТА ИНФОРМАЦИИ В ОБЛАЧНЫХ ВЫЧИСЛЕНИЯХ

  ВАРНОВСКИЙ Н.П., МАРТИШИН С.А., ХРАПЧЕНКО М.В., ШОКУРОВ А.В. — 2015 г.

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