Preview

Труды Института системного программирования РАН

Расширенный поиск
Том 31, № 5 (2019)
Скачать выпуск PDF
7-24
Аннотация

Реализация новой виртуальной процессорной архитектуры в Qemu предполагает создание фронтенда динамического двоичного транслятора TCG для данной процессорной архитектуры. Существующие на сегодняшний день системы тестирования фронтенда TCG используют подход на основе сравнения с эталоном той же процессорной архитектуры. В качестве эталона могут выступать реальный процессор, виртуальная машина с большей точностью эмуляции или другая реализация двоичного транслятора. Однако не всегда такие эталоны доступны, зачастую они могут вообще не существовать. Данная работа нацелена на тестирование реализации процессорной архитектуры в Qemu в условиях отсутствия необходимого эталона для сравнения. Предлагаемый подход основывается на том, что даже для малораспространённой процессорной архитектуры, как правило, доступен пакет binutils и компилятор языка Си. Си-программа может одинаково выполняться на различных процессорных архитектурах, если удаётся избегать в ней ситуаций неопределенного или реализационно зависимого поведения. Это позволяет проводить сравнение хода работы двух разных исполняемых файлов на тестируемой виртуальной машине и машине разработчика. Объектами сравнения такого подхода выступают сущности языка Си, на котором разрабатываются тесты. Подход реализован в программном средстве c2t (CPU Testing Tool) и входит в состав программного комплекса автоматизации разработки моделей устройств и вычислительных машин для Qemu, исходный код которого доступен по адресу https://github.com/ispras/qdt. c2t реализовано на языке программирования Python, поддерживает тестирование Qemu в режиме полносистемной эмуляции и в режиме эмуляции уровня пользователя. Данное средство пригодно как для тестирования фронтендов TCG, полученных с использованием системы автоматизации создания фронтендов TCG, так и реализованных классическим способом (вручную).

25-36
Аннотация
QEMU – широко используемый и достаточно точный эмулятор, способный эмулировать десятки гостевых систем. Эмуляция системы предполагает настройку виртуальных устройств, которые в большом количестве поддержаны в QEMU, что влечет за собой очень длинную и запутанную строку запуска эмулятора. При использовании детерминированного воспроизведения ситуация усложняется не только дополнительными и не вполне очевидными параметрами, но и необходимостью синхронизации строк запуска записи и воспроизведения. Машины могут иметь разный набор устройств в зависимости от платформы и даже версии эмулятора. В статье рассматривается получение информации об устройствах эмулятора QEMU через QEMU Machine Protocol для использования этих данных в графическом интерфейсе. Графический интерфейс QemuGUI поддерживает полный цикл работы с эмулятором: создание и настройка виртуальной машины, запуск в обычном режиме и в режимах детерминированного воспроизведения, взаимодействие с машиной через монитор QEMU.
37-62
Аннотация
В данной работе изучаются теоретические основы автоматической модульной верификации императивных программ с динамической памятью. Вводится формализм композициональной символьной памяти, который используется для построения композиционального алгоритма, порождающего обобщённые кучи. Они являются термами исчисления символьных куч, которые описывают состояния произвольных циклических фрагментов программы. Выводимые в этом исчислении кучи соответствуют достижимым состояниям исходной программы. В работе также устанавливается соответствие между выводом в этом исчислении и исполнением функциональных программ второго порядка без эффектов.
63-78
Аннотация

В настоящее время для языков программирования и процессоров активно разрабатываются модели памяти, направленные на решение различных проблем многопоточного программирования. Так, модель памяти языка OCaml (OCamlMM) позволяет избежать неопределённого поведения, вызванного гонками по данным. Для применения этой модели на практике необходимо доказать корректность её компиляции в распространённые архитектуры процессоров. На данный момент это выполнено для моделей x86 и ARM, но не для Power. Для того, чтобы упростить доказательство корректности компиляции OCamlMM в модель Power, предлагается построить схему компиляции OCamlMM в промежуточную модель памяти (IMM). Для этой модели уже доказана корректность компиляции в модель Power и другие архитектуры, поэтому доказательство корректности компиляции OCamlMM в модель Power сводится к доказательству корректности компиляции OCamlMM в IMM. В данной работе предложена схема компиляции OCamlMM в IMM и доказана её корректность. В этой схеме используются барьеры памяти и инструкции compare-and-swap, которые позволяют исключить поведение, допустимое IMM и запрещённое моделью OCaml. Полученная схема компиляции даёт корректную схему компиляции OCamlMM в модель Power. Кроме того, при таком подходе доказать корректность компиляции OCamlMM в другую архитектуру можно, доказав корректность компиляции IMM в эту архитектуру.

78-88
Аннотация

В статье представлен новый подход для генерации эффективных входных данных для фазз тестирования. Большинство программ перед началом выполнения основного кода проверяют формат входных данных. Часто такие приложения читают служебную информацию из входного файла и определяют поддерживается ли данный формат или нет. Входные файлы, с невалидным форматом отбрасываются. Эффективный фаззинг программ, которые проверяют служебную информацию входных данных является актуальной задачей. Мутация входных файлов часто приводит к генерации невалидной сервисной информации, и программа заканчивается до того, как исполнится ее основной код. Чтобы решить эту задачу, мы разработали и внедрили три специальных плагинов в платформу ISP-Fuzzer. Первый плагин предназначен для собирания трасс выполнения. Второй плагин связывает фрагменты входных данных с выполненными базовыми блоками целевой программы. С помощью этой информации определяются потенциальные интервалы входных данных, которые не должны мутироваться при генерации нового теста. Последний плагин разработан для интервальных мутаций. Эти мутации модифицируют входной файл, оставляя нетронутыми заданные интервалы. Эффективность предложенного метода доказана многочисленными экспериментами.

89-94
Аннотация
В рамках процесса совершенствования экосистемы разработки приложений для различных устройств Huawei компания работает над новым языком программирования. В статье рассматривается подход к реализации OOP в языке программирования, который рассматривается как движение в сторону компонентно-ориентированного программирования.
95-108
Аннотация

Определяются основные методы обеспечения и оценки надежности и безопасности программно-технических систем в процессах их жизненного цикла, a также сбора сведений о возникающих в системах ошибках, дефектах и отказах для последующих изменений. Рассматривается стандартная модель надежности и дается характеристика базовых показателей, среди которых присутствует показатель надежности; функциональность и безопасность составляют основу измерения надежности. Приводится классификация моделей надежности, дается характеристика моделей оценочного типов, используемых при проверке показателей надежности компонентов программно-технических систем. Обсуждаются экспериментальные результаты применения оценочных моделей надежности к разным размерам программных компонентов программно-технических систем и приводится оценка результатов измерения показателя надежности на этих компонентах с учетом плотности дефектов, интенсивности отказов и восстанавливаемости. Отмечается важность обеспечения надежности и безопасности (dependability and safety) систем в рамках новых стандартов интеллектуальных систем и Интернета вещей.

109-126
Аннотация

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

127-136
Аннотация

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

137-144
Аннотация

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

145-152
Аннотация

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

153-164
Аннотация
В докладе рассказывается о результатах применения i-векторных методов распознавания речи для задания расстояния между языками. В качестве входных данных используются фонограммы спонтанной речи. Эксперименты проводятся на звукозаписях латышских и латгальских говоров, но методы применимы и к любым другим идиомам.
165-182
Аннотация

Представлены методы и средства реализации программно-управляемого процесса разработки и верификации формальных моделей требований и проектных решений автоматизированных информационных систем критической информационной инфраструктуры.  Процессы выполняются в единой для всех его участников модельно-языковой и информационно-программной среде автоматизированным способом на основе предметно-ориентированной онтологий. Онтологии описывают  процессы управления качеством программно-технических комплексов на этапах обоснования требований и проектирования систем, разработаны с помощью конструкций и механизмов языков моделирования и проектирования SysML, FUML, OCL, а также математического аппарата сетей Петри, временных автоматов и временных логик. Для валидации и верификации комплекса требований и проектных решений разработаны алгоритмы построения и анализа трассы выполнения модели в среде виртуальной машины VM FUML. Предложены способы интеграции и использования специализированных средств верификации CPN Tools, Rodin, SPIN и Modelica для автоматизированного тестирования моделей комплекса требований и проектных решений.  Данный комплекс обеспечивает более эффективное взаимодействие заказчика и исполнителя как при  разработке требований, так и при проектировании системы, обнаружение и устранение дефектов посредством реализации автоматизированных процедур верификации, валидации и коррекции. Применение данного подхода позволит повысить качество требований и проектных решений, а также улучшить экономические показатели путем снижения финансовых и временных затрат, связанных с выполнением дополнительных работ как в случае обнаружения дефектов, так и при изменении требований или условий эксплуатации.

183-190
Аннотация

Desktop Grid является мощным инструментом высокопроизводительных вычислений. Desktop Grid — это форма распределенной высокопроизводительной вычислительной системы, которая использует время простоя географически распределенных вычислительных узлов, объединенных низкоскоростной сетью. При этом, системы типа Desktop Grid имеют существенные отличия от традиционных вычислительных кластеров и вычислительных GRID и требуют специальных инструментов организации вычислений. В статье представлен механизм динамического прогнозирования времени завершения вычислительного эксперимента в Desktop Grid. Мы предлагаем статистический подход, основанный на линейной регрессионной модели с вычислением доверительного интервала, учетом накопления статистической ошибки и соответствующим — при необходимости — изменением прогноза. На основе предложенного подхода разработан алгоритм прогнозирования и программный модуль для Desktop Grid на базе BOINC. Мы представляем результаты экспериментов, основанные на данных проекта добровольных вычислений RakeSearch.

191-202
Аннотация

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

203-232
Аннотация

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

233-247
Аннотация

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



Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)