Preview

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

Расширенный поиск
Том 29, № 4 (2017)
Скачать выпуск PDF
7-20 67
Аннотация
Элегантный синтаксис языка Ruby заметно усложняет поиск ошибок в больших кодовых базах. Статический анализ усложняется специфическими возможностями языка, такими как динамическое создание методов и исполнение строковых выражений. Даже в языках с динамической типизацией информация о типах важна, так как она позволяет улучшить типобезопасность и производить более надёжные статические проверки того, определён ли метод для объекта и передан ли метода корректный набор аргументов. Одним из путей решения проблемы является использование YARD нотаций. Они позволяют задокументировать входные и выходный типы методов или даже декларировать методы, добавляемые динамически. Такие аннотации позволяют улучшить анализ кода и автодополнение. В статье описывается новый подход к генерации типовых аннотаций. Мы отслеживаем непосредственные вызовы метода во время исполнения программы и сохраняем типы аргументов и выходной тип. На основе собранной информации для каждого метода строится неявная типовая аннотация. Каждому автомату сопоставляется конечный автомат, составленный из различных типовых сигнатур метода. К автомату применяется эффективный алгоритм минимизации с целью снизить затраты на хранение и позволяет привести автомат к виду, который может быть легко представлен в виде регулярного выражения. В сгенерированном автомате учитывается только та функциональность метода, которая была покрыта программой, которую исполнил пользователь. Поэтому в подходе предусмотрено объединение автоматов, полученных у разных пользователей с целью увеличения репрезентативности и покрытия функциональности метода.
21-38 66
Аннотация
Средства и методы process mining позволяют исследовать различные аспекты процессно-ориентированных информационных систем. Как правило, в рамках таких систем несколько исполнителей (агентов) взаимодействуют друг с другом. Поведение агентов, а также механизмы их взаимодействия описываются с помощью моделей процессов. Для моделирования процессов мы применяем обыкновенные сети Петри. Алгоритмы process discovery позволяют восстановить модели реального поведения агентов из журнала событий системы. Однако в случае масштабных систем анализ взаимодействия как поведения отдельных агентов, так и всей системы в целом затруднителен, так как получаемые модели крупномасштабных систем в большинстве случаев крайне громоздкие и плохо читаемые. Для решения этой проблемы мы предлагаем использовать так называемые паттерны интерфейсов, которые описывают, как агенты взаимодействуют друг с другом. С их помощью полная модель мультиагентной системы может быть получена путем композиции отдельных моделей агентов. Кроме того, модели мультиагентных систем, построенные с применением паттернов интерфейсов, позволяет легко идентифицировать поведение каждого отдельного агента. В целях обеспечения корректности применения паттернов интерфейсов мы применяем специальные конструкции на сетях Петри - морфизмы. Результаты эксперимента по применению паттерна для композиционального синтеза модели мультиагентной системы, представленные в работе, показали прирост основных метрик качества по сравнению с моделями, получаемыми с помощью стандартного подхода process discovery.
39-54 56
Аннотация
Верификация многих прикладных систем - в частности, встроенных, - включает в себя процессы, исполняющиеся во времени, для моделирования которых обычно используется временн а я логика, линейная (LTL) или ветвящаяся (CTL). Наиболее развитые автоматические доказатели программ, однако, основаны на невременн ы х теориях: например, на логике Хоара. Возможно ли все же применение этой развитой технологии верификации к более сложным системам? В качестве шага на пути к положительному ответу, мы разработали схему перевода подмножества LTL спецификаций в объектно-ориентированные программы с контрактами на языке Eiffel, которые являются естественными целями для доказателя программ AutoProof. Мы применили эту схему к опубликованной временн о й модели широко используемого реалистичного примера, авиационной системы контроля шасси, являющейся своего рода эталонной задачей для сравнения применимости различных методов спецификации. Верификация переведенной спецификации с помощью AutoProof обнаружила ошибку в одном из временн ы х свойств. Углубленное изучение данной ошибки привело к обнаружению ошибки в опубликованной абстрактной машине состояний (ASM), которая реализует переведенную модель; авторы публикации, в свою очередь, заявили об успешной верификации. Корректировка исходной спецификации и перевод результата в Eiffel с контрактами с последующей верификацией привели к успешному результату. Процесс перевода из LTL в Eiffel все еще находится в зачаточном состоянии и оптимизирован для используемого инструмента верификации (AutoProof), поэтому схема перевода не выглядит простой и элегантной. Даже с учетом указанных ограничений полученные результаты демонстрируют потенциал технологии автоматического доказательства традиционных программ в части ее применимости к специфичным проблемам встроенных систем.
55-72 122
Аннотация
Преобразование Гаусса, также как и его дискретный аналог, является важнейшим инструментом во множестве математических дисциплин и находит свое применение во многих научных и инженерных областях, таких как математическая статистика и теория вероятностей, физика, математическое моделирование, машинное обучение и обработка изображений и прочие. Ввиду высокой вычислительной сложности преобразования Гаусса (квадратичная сложность относительно количества точек и экспоненциальная - относительно размерности точек), необходимы эффективные и быстрые методы его аппроксимации, обладающие большей точностью по сравнению с существующими ныне методами, такими как Быстрое Преобразование Фурье или оконное преобразование. В данной статье предложен новый метод аппроксимации преобразования Гаусса для равномерно распределенный множеств точек (например, двумерных изображений), основанный на использовании L 2 метрики и метода разделения доменов. Такой подход позволяет значительно сократить количество вычислительных операций путем выполнения предварительных вычислений, и снизить вычислительную сложность метода до линейной. Результаты ряда численных экспериментов показали, что разработанный алгоритм позволяет получить более высокую точность аппроксимации без потери скорости вычисления в сравнении со стандартными методами. Также в качестве примера применения предлагаемого алгоритма была разработана новая схема смежной фильтрации изображения. Было показано, что новый фильтр на основе быстрого L 1 преобразования Гаусса позволяет получить результат более высокого качества при сопоставимой скорости вычисления и при этом избежать появления нежелательных артефактов в результате обработки, таких как эффект ореола.
73-86 120
Аннотация
Данная статья описывает текущие исследования по цифровой стабилизации видеоизображения в режиме реального времени с использованием MEMS датчиков. Авторы предполагают использование данного метода для стабилизации видеоизображения, передаваемого оператору дистанционно управляемых мобильных роботов, в частности, для улучшения качества управления малыми летательными аппаратами и снижения усталости оператора. В статье вводятся основные математические модели и понятия необходимые для реализации программного модуля цифровой стабилизации с использованием показаний MEMS датчиков. К таким моделям необходимо отнести: модель вращения камеры, модель трансформации кадра и модель rolling shutter эффекта. Также в статье рассматриваются существующие подходы к стабилизации видеоизображения с использованием MEMS датчиков и дается оценка их применимости в режиме реального времени. Кроме того, освещаются проблемы, возникающие при воспроизведении результатов предыдущих работ и неразрешенные в данных статьях. К таким проблемам следует отнести: синхронизацию показаний датчиков и кадров, калибровку камеры и датчиков, повышение точности определения вращения камеры, эффективную трансформацию кадра при повороте. Авторы предлагают возможные решения данных проблем, в частности, одним из результатов является система параллельной синхронизированной записи кадров и показаний датчиков движения - гироскопа и акселерометра - на базе операционной системы Android. В качестве основного результата представляется фреймворк для тестирования алгоритмов по стабилизации видеоизображения, а также реализация алгоритма стабилизации с использованием фильтра Гаусса для сглаживания траектории движения камеры в рамках данного фреймворка.
87-106 58
Аннотация
За последние несколько лет возник значительный интерес к мобильным приложениям, ориентированным на построение маршрутов пользователей гаджетов; в таких приложениях наряду с важной функцией навигации также возможно отправление своевременных оповещений о прибытии к заданному месту назначения. Несмотря на большой объем имеющейся информации о специфике навигационных сервисов, актуальным остается вопрос относительно точности позиционирования. В данной статье рассматривается возможный подход к решению проблемы сравнения, связанного с определением близости пользователя к конечной станции его маршрута в метро. Такая близость определяется путем подсчета разницы в координатах между текущей позицией пассажира и фиксированной точкой. С целью создания Системы Рекомендаций Маршрутов (СРМ) была применен аппарат нечеткой логики, который использует лингвистические переменные для выражения имеющейся нечеткости (неопределенности) в понимании/восприятии вербального понятия «близость к …». В работе подробно объясняется каждая переменная, используемая в системе нечеткого вывода (англ. FIS), а также представляется набор нечетких правил ЕСЛИ-ТО модели. Для проверки стабильности модели (пока имеет смысл говорить о прототипе модели как первом шаге на пути дальнейшей ее проработки и изменения), основанной на схеме логического вывода Мамдани, рассматриваются несколько тестовых экспериментов с моделью, описываются получаемые результаты. В дальнейшем, планируется разработка мобильного Android-приложения, нацеленного на построение маршрутов городского общественного транспорта с возможностью использования представленной модели при реализации функции по отправлению своевременных оповещений о приближении к пункту назначения. Следует отметить, что акцент делается на использовании в модели интервальных нечетких множеств второго типа (англ. IT2FS), которые привлекают значительное внимание исследователей в настоящее время. Значимость задачи разработки подобных моделей определяется, в первую очередь, необходимостью адекватного учета тех факторов, которые по своей сути являются нечеткими (неопределенными). Данная работа, по мнению авторов, может помочь в продолжении и развитии исследований, связанных с этой же или подобными темами.
107-122 131
Аннотация
Задачи маршрутизации важны для областей логистики и управления трансортом. Задачи маршрутизации в основном связаны с определением оптимального набора путей в мультиграфе. Задача китайского почтальона (CPP) является особым случаем задачи маршрутизации, имющим много потенциальных приложений. Мы предлагаем решение MCPP (специального NP-полного случая CPP на смешанном мультиграфе) с использованием редуцирования исходной задачи к обобщенной задаче коммивояжера (General Traveling Salesman Problem, GTSP). Указываются варианты CPP. Представлены математические формулировки некоторых проблем. Показан алгоритм редуцирования MCPP в мультиграфе к GTSP. Приводятся экспериментальные результаты решения MCPP в мультиграфе посредством редуцирования к GTSP.
123-138 252
Аннотация
Задача коммивояжера - одна из важнейших задач теории графов и комбинаторной оптимизации, суть которой состоит в нахождении гамильтонова цикла наименьшей длины. Разработка методов для решения задачи коммивояжера осуществляется на протяжении многих лет, и, по-прежнему, остается актуальной, поскольку задача является NP-трудной. Решения применяются, в основном, для минимизации производственных и логистических затрат и издержек. В работе рассматривается частный случай общей постановки задачи коммивояжера, в котором выполняется свойство метрики - метрическая задача коммивояжера. Целью данной работы является определение группы Парето оптимальных алгоритмов решения метрической задачи коммивояжера по критериям времени работы и точности решения в ходе экспериментального исследования. В связи с тем, что задача коммивояжера является NP-трудной, в работе рассматриваются только эвристические алгоритмы, позволяющие получить приближенные решения за полиномиальное время. В статье представлено краткое описание используемых алгоритмов решения метрической задачи коммивояжера, указаны их априорные точностные и временные оценки. Приведено описание плана эксперимента. Данными для экспериментального исследования послужили два набора из открытой библиотеки данных для метрической задачи коммивояжера, основанные на высоко-интегральных вычислительных схемах (VLSI Data Sets) и географических координатах (высоте и широте) городов в различных странах (National TSPs). В результате исследований выявлены оптимальные по Парето алгоритмы для наборов данных различных размерностей - до 700 тысяч вершин. Для каждого N в число Парето-оптимальных алгоритмов входят некоторые из алгоритмов MC, SC, NN, DENN, CI, GRD, CI + 2-Opt, GRD + 2-Opt, CHR и LKH. Приведена таблица, содержащая информацию о результатах экспериментов.
139-154 63
Аннотация
Конечные автоматы широко используются для анализа и синтеза управляющих систем. При описании систем, поведение которых зависит от времени, конечный автомат расширяется введением временных аспектов и вводится понятие временного автомата. В настоящей работе мы рассматриваем проблему минимизации автоматов с таймаутами и временными ограничениями, поскольку сложность многих задач в теории автоматов существенно зависит от размеров исследуемой системы. Поведение временного автомата может быть достаточно точно описано соответствующим конечным автоматом, и предлагаемый метод минимизации числа состояний системы основан на использовании такой конечно автоматной абстракции. Более того, далее мы минимизируем и временные аспекты автоматного описания, сокращая продолжительность таймаутов и число переходов с временными ограничениями. Мы также показываем, что для полностью определённого детерминированного временного автомата существует единственная минимальная (каноничная) форма, т. е. единственный приведённый по состояниям и временным аспектам автомат с таймаутами и временными ограничениями, поведение которого совпадает с исходным временным автоматом; например, такая минимальная форма может быть использована при построении проверяющих тестов для проверки функциональных и нефункциональных требований к тестируемой реализации. Предложенный метод к минимизации временных аспектов на основе конечно автоматной абстракции может быть применён и для частных случаев рассматриваемой модели, т. е. для минимизации детерминированных полностью определенных автоматов только с таймаутами или только с временными ограничениями.
155-174 75
Аннотация
В данной статье мы предлагаем метод автоматического построения так называемых «гибридных» UML-моделей, что относится к области извлечения и анализа процессов ПО. Модели строятся на основе трасс исполнения, представленных в виде журналов событий, систем с сервис-ориентированной архитектурой (СОА). В то время как известные техники обратной разработки обычно используют исходный программный код, который часто недоступен, наш подход работает с журналами событий, записываемыми большинством информационных систем, и некоторыми эвристическими параметрами. Так как отдельный класс UML-диаграмм представляет только одну перспективу модели системы, мы предлагаем синтезировать комбинацию нескольких классов UML-диаграмм (последовательности и деятельности), которые рассматриваются совместно с диаграммами коммуникаций. Это позволяет повысить выразительную силу отдельной «гибридной» диаграммы. Каждый класс диаграмм представляет один из уровней абстракции (workflow, operation и interaction), которые обычно используются при рассмотрении взаимодействия web-сервисов. Предлагаемый алгоритм состоит из четырех этапов: разделение журнала событий на несколько частей, построение UML диаграмм последовательности, деятельности и коммуникаций. Мы также предлагаем инкапсулировать некоторые незначительные или низкоуровневые имплементационные детали (например, внутренние операции сервисов) в диаграммы деятельности и соединять их с более высокоуровневыми диаграммами последовательности с использованием «interaction use» фрагментов. Чтобы решить проблему больших размеров синтезируемых UML диаграмм последовательности, мы предлагаем обобщающую технику, основанную на регулярных выражениях. Предложенный подход оценен с использованием разработанного программного инструмента в виде Windows-приложения, написанного на языке C#. Этот инструмент строит UML модели и сохраняет их в виде XML-файлов. Такие файлы совместимы с хорошо известным интрументом проектирования программной архитектуры Sparx Enterprise Architect, в котором синтезированные модели могут быть визуализированы и отредактированы.
175-190 49
Аннотация
Вполне структурированные системы переходов являются хорошо известным инструментом для доказательства разрешимости свойств покрываемости и ограниченности. Каждый год появляются новые формализмы, которые оказываются вполне структурированными системами переходов. Несмотря на большой объем теоретической работы, существует большая потребность в эмпирических изучении вполне структурированных систем переходов. В данной работе представлен инструмент для анализа таких систем. Мы предлагаем расширение высокоуровневого языка SETL для описания вполне-структурированных систем переходов. Это позволяет описывать новые формализмы близко к их формальному определению. Таким образом упрощается создание и изменение новых формализмов, а также осуществление анализа поведенческих свойств без большого объема программистских усилий. Это удобно, когда новый формализм находится в стадии изучения и разработки. Были реализованы два самых изученных алгоритма анализа поведения вполне структурированных систем переходов (обратный алгоритм и анализ конечных деревьев достижимости). Их производительность была измерена на моделях сетей Петри и систем с потерей сигналов. Разработанный инструмент может быть полезным при внедрении и тестировании методов анализа формализмов, которые оказываются вполне структурированными системами переходов.
191-202 108
Аннотация
В данной работе рассматривается марковский анализ моделей комплексных программно-аппаратных систем. Инструмент марковского анализа может быть использован, в частности, для верификации моделей систем интегральной модульной авионики. Во введении перечисляются основные достоинства и недостатки марковского анализа. К примеру, марковский анализ, в отличие от других подходов - анализа дерева неисправности и анализ алогической схемы, позволяет анализировать модели систем, способных к восстановлению. Основным недостатком данного подхода является экспоненциальный рост размера моделей в зависимости от числа компонентов в анализируемой системе. Это существенно ограничивает возможность применения марковского анализа на практике. Другой важной проблемой является создание нового алгоритма трансляции исходной модели системы в модель, пригодную для марковского анализа (марковскую цепь), так как существующие решения накладывают существенные ограничения на архитектуру анализируемой системы. Далее идет краткое описание контекста, в котором инструмент должен работать - язык моделирования AADL с библиотекой Error Model Annex, набор инструментов MASIW, а также описывается сам метод марковского анализа. В основной части предлагается алгоритм трансляции модели системы в марковскую цепь, частично решающий проблему экспоненциального роста марковской цепи. Затем следует описание дальнейших шагов, а также предлагаются эвристики, позволяющие значительно сократить время работы итоговой программы. В работе также рассматриваются существующие инструменты марковского анализа и их недостатки. В качестве результата данной работы предлагается новый инструмент марковского анализа, который может быть эффективно использован на практике.
203-216 87
Аннотация
Верификация программного обеспечения - вид деятельности, направленный на контроль качества программного обеспечения и обнаружения ошибок в нем. Статическая верификация - это один из способов верификации, который производится без выполнения исходного кода программы. Для статической верификации используется специальное программное обеспечение: инструменты статической верификации, которые часто работают с исходным кодом программы. Одним из таких инструментов является инструмент под названием CPAchecker. Проблема его текущей модели памяти заключается в том, что при встрече функции, возвращающей указатель на область памяти, у которой отсутствует тело, в процессе верификации о ее возвращаемом значении могут быть сделаны произвольные предположения. Несмотря на то, что они теоретически допустимы, вероятность их выполнения на практике очень низка. Использование этих предположений может привести к ложному предупреждению в качестве результата верификации. В данной статье мы делаем обзор на один из подходов, благодаря которому можно избавиться от такой проблемы, а также предлагаем формальное описание данного подхода в терминах формул путей, содержащих неинтерпретируемые функции, которые инструмент использует для моделирования памяти программы. Также мы приводим результаты сравнительного анализа эффективности предложенной реализации относительно существующей модели памяти.
217-230 55
Аннотация
Ядро операционной системы Linux - это частый пример современных инженерных решений в области создания продуктовых линеек программного обеспечения. Сегодня это одна из наиболее сложных программных систем. Для того, чтобы обеспечить наиболее безопасное построение вариантов продуктовой линейки, необходимо анализировать конфигурационный файл Kconfig помимо исходного кода. Ядро содержит десять тысяч вариабельных переменных несмотря на современную инженерию. Исследователи в области верификации предлагают большое количество решения проблемы анализа. Стандартные процедуры верификации здесь не могут быть применены из-за времени проверки покрытия всех конфигураций. Мы предлагаем инструмент, который базируется на связи уже существующих программах для проверки кода и конфигурационного файла с метрикой покрытия. Такой пакет - это эффективный инструмент для расчета всех допустимых конфигураций для предопределенного набора кода и Kconfig. Предложенные методы могут быть использованы для улучшения существующих инструментов анализа, а также для выбора правильной конфигурации. Наша основная цель - лучше разобраться в возможных дефектах и предложить быстрое и безопасное решение для проверки ядра Linux. Это решение будет описано как программа с инструкцией по реализации внутренней архитектуры.
231-246 53
Аннотация
В статье представлена методика масштабируемой функциональной верификации протоколов когерентности памяти, которая основана на методе верификации, который ранее был разработан автором статьи. Масштабируемость при верификации означает независимость работ по верификации от размера модели, то есть от количества процессоров верифицируемой системы. В статье предложен подход к разработке формальных моделей протоколов когерентности памяти на языке Promela. Приведены примеры описаний, взятые из модели протокола когерентности памяти системы Эльбрус-4С. Результирующие формальные модели отражают представление протоколов когерентности памяти, используемое разработчиками таких протоколов - в виде множества взаимодействующих конечных автоматов. Описана разработка программного инструмента, написанного на языке С++ с использованием библиотеки Boost.Spirit в качестве генератора синтаксических анализаторов. Программный инструмент позволяет автоматизировать выполнение синтаксических преобразований Promela-моделей. Выполнение данных синтаксических преобразований происходит в соответствии с методом верификации. В статье представлена процедура уточнения модифицированных моделей, основанная на введении в модель вспомогательных переменных. Использовать эту процедуру предлагается в том случае, когда при верификации возникают ложные сообщения об ошибках, для устранения таких сообщений. Представлена методика верификации, которая состоит из следующих шагов: разработка исходной модели протокола когерентности памяти на языке Promela, автоматизированное преобразование данной модели согласно методу верификации, верификация модифицированной модели с помощью инструментального средства Spin, анализ отчета о верификации, сгенерированного инструментом Spin. Изложенная методика была успешно применена для верификации протокола когерентности памяти семейства MOSI, реализованного в микропроцессорной системе Эльбрус-4С. Экспериментальные результаты показали, что затраты процессорного времени и памяти на проведение параметризованной верификации незначительны, а требуемый объем ручной работы приемлем. Для уточнения модифицированной модели протокола системы Эльбрус-4С понадобилось ввести лишь две вспомогательные переменные.
247-256 75
Аннотация
Тестирование аппаратуры - это процесс, нацеленный на обнаружение неисправностей, внесенных в интегральные схемы в процессе производства. Для оценки качества таких тестов используют две основные метрики: способность обнаруживать ошибки (покрытие ошибок) и время тестирования (длина теста). Известно множество методов генерации тестов, однако масштабируемого решения, применимого к сложной цифровой аппаратуре, нет до сих пор. В данной статье анализируется возможность использования функциональных тестов, построенных по высокоуровневым моделям (прежде всего, моделям уровня регистровых передач), для низкоуровневого производственного тестирования. Рассматривается конкретный метод генерации тестов, использующий технику проверки моделей (model checking). Входной информацией выступает HDL-описание. Метод состоит из двух ключевых шагов: построение модели системы и построение модели покрытия. Указанные модели автоматически извлекаются из HDL-описания. Модель системы представлена в виде высокоуровневых решающих диаграмм. Модель покрытия - это множество LTL-формул, определяющих условия достижимости переходов расширенного конечного автомата, описывающего систему. Построенные модели транслируются во входной формат инструмента проверки моделей (model checker), который для каждой формулы модели покрытия генерирует контрпример - вычисление, нарушающее эту формулу, то есть приводящее к срабатыванию соответствующего перехода автомата. Изначально рассматриваемый метод предназначался для покрытия всех путей исполнения HDL-описания и обнаружения недостижимого кода. Экспериментальное сравнение метода с существующими аналогами показало, что он строит более короткие тесты, однако эти тесты достигают меньшего уровня покрытия константных неисправностей, чем тесты, построенные с помощью специальных средств. В статье предлагается модификация метода для преодоления указанного недостатка.
257-268 40
Аннотация
В статье приведены подходы, использовавшиеся в процессе верификации контроллеров 10 гигабитного Ethernet, разработанных в АО «МЦСТ». Описаны принципы работы устройств - они предоставляют программисту набор регистров, отображаемых в память, а также используют прямой доступ к памяти. Представлен набор подходов, применяемых при верификации подобных устройств - верификация физического прототипа, системная и автономная верификация. Описана мотивация выбора подхода - комбинации системной верификации целого устройства и автономной верификации одного из его компонентов. В статье дано описание тестовых систем, использовавшихся для верификации устройств. Тестовая система всего устройства осуществляет передачу Ethernet пакетов в сеть и их прием из сети. Разработаны и описаны алгоритмы преобразования пакетов в представление, используемое устройством. Для модулей связи между внутренними пакетными шинами и внешним интерфейсом была разработана автономная тестовая система. При разработке тестовых систем использовалась методология UVM. Выбранная методология, а также предложенные структуры тестовых систем позволили использовать одни и те же компоненты в различных тестовых системах. Приведен набор тестовых сценариев, разработанных для тестовых систем. Особо важным является процесс верификации пропускной способности устройства. Описаны методы, использовавшиеся для измерения пропускной способности устройства, а также режимы работы контроллера, в которых проводилось измерение. Представлены текущие значения пропускной способности устройства, которых удалось достигнуть в различных режимах. В заключение приведен список найденных ошибок, а также описаны те функции устройства, на которые они влияли, а также направления дальнейшей работы.
269-282 103
Аннотация
Для правильной обработки информации о возможных сделках, проходящих через торговые платформы, выявления и предупреждения финансовых манипуляций, биржи устанавливают системы контроля и мониторинга данных. Эти системы получили широкое распространение за последние годы. Объемы и темпы торговли постоянно возрастают, увеличивается число разновидностей ценных бумаг. Финансовые регуляторы предъявляют все новые требования к торговым платформам. Из вышесказанного следует, что современные финансовые информационные системы в ближайшие годы будут продолжать совершенствоваться и активно использовать средства машинного обучения. Поэтому в последние несколько лет системы контроля и мониторинга рынка начинают внедрять модули интеллектуального анализа транзакций. Таким образом, интеллектуальные системы контроля и мониторинга рынка требуют усовершенствования подходов к их тестированию. Это связано с тем, что методы интеллектуального анализа данных формируют свои собственные зависимости между переменными. Тестовые сценарии должны разрабатываться таким образом, чтобы ожидаемый результат был понятен и предсказуем. Очевидно, что стандартные методы тестирования требуют модернизации. В представленной статье рассмотрены особенности современных интеллектуальных информационных систем, а также особенности их тестирования. В данном исследовании был разработан прототип модуля классификации финансовых манипуляций. Также предложены тестовые сценарии, позволяющие тестировать разработанный прототип. Данные сценарии состоят из нескольких типов, основанных на методологии классов эквивалентности. Разделение на классы эквивалентности было выполнено после анализа реальных данных. Прототип был протестирован с помощью выше обозначенных сценариев. Предложенный метод позволил выявить недостатки модуля классификации финансовых манипуляций.
283-294 68
Аннотация
Современные операционные системы для встроенных систем могут использоваться для решения задач управления в различных аппаратных контекстах. Управляющие ЭВМ могут различаться архитектурой центрального процессора, составом каналов связи, поддерживаемыми протоколами связи и т. д. Обычно встраиваемые ОС конфигурируются на этапе сборки, позволяя создать образ ОС, предназначенный для выполнения на определенной аппаратной платформе. Эту конфигурацию осуществляет команда, называемая группой системной интеграции. Зачастую ОС для встроенных систем разрабатываются множеством компаний. Если ОС не является модульной, то совместные проектирование, разработка и конфигурирование ОС представляют собой очень сложным задачи. Поддержка модульности и компонентой сборки значительно уменьшает необходимость во взаимодействии между компаниями-разработчиками. Клиентам это позволяет создавать минимальные решения, оптимально адаптированные под особенности задачи и аппаратной платформы. Кроме того, различные производители систем могут быть заинтересованы в том, чтобы внедрять в решение свои специализированные компоненты, в том числе и в бинарном виде, защищающем интеллектуальную собственность разработчиков. В данной статье мы представляем подход к построению модульных решений из гетерогенных компонентов на базе ОС РВ JetOS. Разработанный нами механизм связывания компонентов позволяет объединять гетерогенные компоненты от различных производителей в рамках одного раздела адресного пространства. Этот механизм позволяет разработчикам компонентов осуществлять независимую разработку. А системному интегратору позволяет независимо от разработчиков конфигурировать ОС, выбирая какие компоненты попадут в конечный образ ОС, и как эти компоненты будут взаимодействовать.
295-302 70
Аннотация
В этой статье мы расскажем о проекте по разработке отладчика для мультиплатформенной операционной системы реального времени JetOS, созданной для гражданских авиационных систем. Она предназначена для работы в рамках архитектуры Интегрированной Модульной Авионики (ИМА) и реализует ARINC 653 спецификацию API. Эта операционная система разрабатывается в институте системного программирования РАН, и важным шагом в ее создании является разработка инструмента для отладки пользовательских приложений. В этой статье будут рассмотрены проблемы особенностей отладчика для операционной системы реального времени и показаны методы, которыми достигается его мультиплатформенность, а также легкая переносимость на новую платформу. Более того, были рассмотрены другие отладчики для встраиваемых операционных систем, такие как CodeWarrior, отладчики для WxWorks и L4Ka::Pistachio, а также был изучен их функционал. В заключение мы представим наш отладчик, который может работать как в эмуляторе QEMU, используемом для эмуляции окружения для JetOS, так и на целевой машине на всех поддерживаемых платформах. Представленный отладчик является удаленным и построен с использованием структуры GDB, но содержит ряд расширений, специфичных для отладки встроенных приложений. Сама структура отладчика была разделена на архитектурно зависимые и независимые части, что помогает облегчить перенос отладчика на новую платформу. В то же время наш отладчик удовлетворяет большинству требований, налагаемых к отладчику операционной системы реального времени, а также уже используется разработчиками приложений для Jet OS.
303-314 58
Аннотация
При создании документации программного обеспечения часто применяется копирование и вставка с последующим редактированием, в результате чего возникает много повторяющегося текста. Такие повторы усложняют и удорожают поддержку документации, особенно в случае длительных жизненных циклов программного обеспечения и документации. Ещё более усложняет ситуацию то, что зачастую информация повторяется приблизительно, т.е. одна и та же информация может быть многократно представлена с разными уровнями детализации, в различных контекстах и т.д. В данной работе предложен алгоритм, предназначенный для обнаружения неточных повторов в документации программного обеспечения. Алгоритм основан на модели N-грамм и реализован с использованием Natural Language Toolkit. Алгоритм апробирован на документации нескольких проектов с открытым исходным кодом.
315-324 63
Аннотация
Ежедневно пользователями социальных сетей генерируются значительные объемы текстового контента, который дополнительно содержит информацию о координатах и времени публикации. Эти данные могут быть проанализированы и использованы для оценки общего состояния большой популяции пользователей с целью решения научных вопросов из широкого спектра дисциплин. В данной статье описывается разработка программы для мониторинга общественных настроений на основе анализа тональности сообщений из русскоязычного сегмента социальной сети Twitter с использованием методов машинного обучения. В разработанном программном продукте была использована многоуровневая сетевая архитектура «клиент-сервер». Написанное на Python серверное приложение собирает сообщения пользователей через Twitter API, осуществляет предварительную обработку текста, анализирует эмоциональную окраску сообщений с использованием мультиномиального наивного Байесовского классификатора и определяет их принадлежность к административно-территориальным субъектам страны. Клиентское веб-приложение визуализирует результаты анализа тональности, которые состоят из карты настроений России, где для каждого административно-территориального субъекта указывается текущий показатель настроения, а также из графиков изменения настроения в течение дня и в течение недели. В процессе разработки программного средства были задействованы облачные сервисы. Серверная часть была развернута на платформе Google App Engine, которая позволяет выполнять веб-приложения на серверах Google, то есть полностью абстрагироваться от инфраструктуры, поэтому при работе сервер не нуждается в администрировании. Данные программы хранятся в облачной базе данных Google Cloud Datastore, которая полностью интегрирована с Google App Engine.
325-336 72
Аннотация
В интернете все большую популярность приобретают СМИ, отказывающиеся от общепринятого формального способа изложения новостей и делающие акцент на креативности предоставляемого контента. Яркими примерами могут послужить паблик "Лентач" из социальной сети "ВКонтакте", сопровождающий каждую новость мемами, и ресурс "КАКТАМ?", оборачивающий заголовки в намеренно сверхэмоциональную форму. Мы решили реализовать инструмент Narrabat, пересказывающий новости в еще одном необычном стиле. Его задача - преобразовывать новостные ленты, взятые из сторонних источников, в небольшие стихотворения, отражающие ключевые события новостных сюжетов. В качестве основы для генерации стихов используется большая коллекция русской классики (состоящая из, к примеру, произведений Блока и Некрасова). Одним из главных достоинств выбранной нами формы пересказа и созданного инструмента в частности является то, что, при всей оригинальности вывода, процесс его генерации полностью автоматизирован, в отличие от сервисов, описанных выше. Инструмент работает в несколько этапов: сначала происходит выделение фактов из заголовков выгруженных новостей при помощи Tomita Parser, после чего факты передаются в модуль, отвечающий за генерацию стихотворения. По ходу работы мы использовали несколько подходов для генерации стихотворений, такие, как алгоритмы, построенные на правилах, и машинное обучение, включая нейронные сети. На данном этапе наилучший результат дал первый метод, однако работа по обучению нейронной сети ведется до сих пор. В данной статье мы опишем текущие результаты работы, приведем примеры сгенерированных стихотворений, а также перечислим направления для дальнейшего улучшения инструмента.


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


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