научный журнал по математике Программирование ISSN: 0132-3474

БОЖЕНКОВА Е.Н. — 2012 г.

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

ЗЕЛЕНОВ С.В., КОСТЫЧЕВ Е.А., ОМЕЛЬЧЕНКО В.А. — 2012 г.

Приложения, обрабатывающие большие массивы данных, являются широко распространенным типом программного обеспечения. В частности, такие приложения решают задачи интеграции данных в области интеграции корпоративных приложений. При решении таких задач используются специальные инструментальные среды, поддерживающие разработку, выполнение и мониторинг приложений, реализующих шаблон извлечения, трансформации и загрузки данных (Extract, Transform and Load-ETL). Специфика функционального тестирования таких приложений заключается в большом количестве возможных комбинаций входных данных. Подходы, реализованные в инструментах генерации данных для функциональной проверки приложений над базами данных, в лучших случаях основываются на схемах баз данных и запросах на SQL, используемых в тестируемых приложениях. Гарантированное покрытие функциональности тестируемого приложения при таких подходах может быть достигнуто только полным перебором возможных комбинаций исходных данных. При помощи предложенного в статье подхода к генерации данных возможно достижение покрытия функциональности приложения с близким к оптимальному объему данных (один набор данных для одной функциональной ветви приложения).

КОРОТКОВ А.Е. — 2012 г.

Хранение пространственных запросов и обработка пространственных запросов - важные задачи современных баз данных. Эффективное выполнение пространственных запросов зависит от используемой индексной структуры. R-дерево - широко известная пространственная индексная структура. Существуют различные версии R-дерева, и одно из наиболее частых отличий версий между собой - алгоритм разделения узла. Проблема разделения узла в одномерном R-дереве может показаться слишком тривиальной, чтобы рассматриваться отдельно. Одномерные интервалы могут быть легко разделены на основе сортировки. Некоторые алгоритмы разделения узла для R-дерева для двух и более измерений содержат в своем составе одномерное разделение. Однако, если рассмотреть вопрос более детально, существующие алгоритмы для одномерного разделения работают не идеально в некоторых сложных случаях. В данной работе вводится новый алгоритм разделения узла, основанный на двух сортировках, которые позволяет обрабатывать некоторые сложные одномерные разделения лучше. Также вводится алгоритм разделения узла для двух-и более мерных R-деревьев, который основан на предложенном одномерном алгоритме. Тесты выявляют значительно лучшее поведение предложенных алгоритмов по сравнению с известными в случае сильно пересекающихся данных.

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

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

ГАНЖА Е.И. — 2012 г.

Реализованные в современных системах компьютерной алгебры алгоритмы решения линейных уравнений с частными производными обычно ограничены случаем уравнений с двумя независимыми переменными. В данной работе предложено обобщение теории преобразований Лапласа на дифференциальные операторы второго порядка в R3 (и более общо, в Rn) с главным символом, разлагающимся в произведение двух линейных по производным множителей. Рассмотрено два алгоритма таких обобщенных преобразований Лапласа и описаны классы операторов в R3, к которым они применимы. Исправлена ошибка в работе [8] и показано, что преобразование Дини является преобразованием Лапласа для оператора с коэффициентами из некоммутативного тела Оре.

КАПЦОВ О.В. — 2012 г.

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

ПОНОМАРЕНКО А.В., РУБАНОВ В.В. — 2012 г.

В данной статье рассматриваются проблемы контроля обратной совместимости между новыми и старыми версиями базовых программных компонентов (библиотек). Окружение Linux рассматривается в качестве основного примера. Нарушение обратной совместимости в новых версиях программных компонентов может привести к некорректной работе (на бинарном уровне) или невозможности перекомпиляции (на уровне исходных кодов) пользовательских приложений, нацеленных на использование предыдущих версий, при попытке перехода на новую версию компонента. В статье описаны типичные причины, приводящие к нарушению обратной совместимости на бинарном уровне, а также представлен новый подход к автоматическому выявлению этих причин на стадии разработки программных компонентов (основное внимание уделено анализу изменений в структуре интерфейсов). Языки Си/CH-+ взяты за основу для демонстрации подхода, хотя предлагаемый подход может быть применен и к другим языкам программирования, таким как Java или языкам из Microsoft Visual Studio (С#, Visual Basic и др.). В отличие от существующих аналогов, предлагаемый подход может выявлять широкий спектр проблем обратной совместимости благодаря анализу изменений в сигнатурах функций и определений типов данных, извлекаемых из заголовочных файлов компонентов в дополнение к анализу символов исполняемых файлов. Также в данной статье рассмотрен инструмент, реализующий предлагаемый подход, и результаты практического применения этого инструмента. Шаги к дальнейшему улучшению качества автоматической верификации обратной совместимости обсуждаются в заключении.

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

Статический верификатор BLAST является одним лучших открытых верификаторов, работающих с программами на языке Си. В статье описываются принципы реализации BLAST, те ограничения, которые выявились при его практическом использовании для верификации драйвером ОС Linux и опыт развития BLAST, получений в проекте LDV (Linux Driver verification) [3].

ГОРБЕНКО А.А., ПОПОВ В.Ю — 2012 г.

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

ЗИНИН М.В. — 2012 г.

В данной работе для двух систем компьютерной алгебры - REDUCE и Macaulay2 - представлен пакет BIBasis, позволяющий вычислять булевы инволютивные базисы и базисы Грёбнера. В соответствующих разделах описаны реализации и пользовательские интерфейсы пакета для каждой из систем. Также приводятся результаты сравнения пакета BIBasis с другими доступными в данных системах компьютерной алгебры пакетами и алгоритмами для построения булевых базисов Грёбнера.

ШЕМЯКОВА ЕКАТЕРИНА — 2012 г.

Работа посвящена преобразованиям Дарбу - эффективному алгоритму нахождения аналитических решений дифференциальных уравнений с частными производными. Нам удается доказать, что Вронскиан-формулы, предложенные Г. Дарбу для линейных операторов второго порядка на плоскости описывают все возможные дифференциальные преобразования с M вида Dx + m(x, y) и Dy + m(x,y) за исключением преобразований Лапласа.

ЧУПИЛКО М.М. — 2012 г.

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

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

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

ВЕБСТЕР К., ВОЛЬФ Т., ШРЮФЕР Э. — 2012 г.

В статье описывается пакет LSSS (Linear Selective Systems Solver) системы компьютерной алгебры REDUCE, предназначенный для решения линейных алгебраических систем с рациональными коэффициентами. Данный пакет особенно эффективен при решении очень больших разреженных систем, имеющих решение, в котором многие переменные равны нулю. Описано применение пакета для исследования одного неабелевого лорановского ОДУ (обыкновенного дифференциального уравнения), недавно введенного М. Концевичем. Вычисления симметрий с помощью данного пакета подтверждают, что найденная ранее для этой системы пара Лакса порождает все первые интегралы по крайней мере до степени 14.

ВАСИЛЬЕВ С.А., ИЛЮШИН А.И., ОЛЕНИН М.А. — 2012 г.

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

2012

АБРАМОВ С.А., БОГОЛЮБСКАЯ А.А., РОСТОВЦЕВ В.А. — 2012 г.

КОГАЛОВСКИЙ М.Р. — 2012 г.

Исследования, направленные на обеспечение семантического доступа к базам данных, имеют многолетнюю историю и начались еще на ранних стадиях развития технологий баз данных. К сожалению, они все еще не привели к созданию широко распространенных индустриальных технологий. В последнее десятилетие деятельность консорциума W3C в области Семантического Веба и создание стандартов языков описания онтологий вызвали новую волну активности в разработках инструментария для систем семантического доступа к базам данных и нового класса систем баз данных, называемых системами доступа к данным, основанными на онтологиях (OBDA-системам). В таких системах онтологии используются в качестве концептуальной схемы предметной области и основы пользовательского интерфейса для SQL-систем баз данных. Предложенные в последние годы подходы не обеспечивают "окончательного" решения проблемы. Тем не менее, удалось создать языки описания онтологий, позволяющие достигнуть приемлемого компромисса между их выразительностью, которая остается достаточной для многих приложений, и вычислительной сложностью рассуждений на онтологиях и обработки запросов данных, хранимых в больших базах данных. Созданы предпосылки для появления индустриальных технологий разработки систем указанного класса. В предлагаемой работе приводится обзор полученных в последние годы основных результатов исследований и разработок в рассматриваемой области.

ВАСЕНИН В.А., КРИВЧИКОВ М.А. — 2012 г.

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

КЛЮЧНИКОВ И.Г., РОМАНЕНКО С.А. — 2012 г.

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