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

В данной работе представлен метод анализа и верификации моделей Use Case Maps (UCM) с конструкциями управления сценариями 뜨 защищенными компонентами и конструкциями обработки ошибок. Анализ и верификация UCM моделей проводится с помощью раскрашенных сетей Петри (РСП) и верификатора SPIN. Приводятся описания алгоритмов трансляции UCM в РСП и РСП во входной язык Promela системы SPIN. Впервые представлены оценки для количества элементов результирующих РСП моделей в зависимости от количества элементов исходных UCM моделей с конструкциями управления сценариями, а также количества состояний Promela моделей. Представленный метод анализа и верификации демонстрируется на примере верификации программы обновления прошивки маршрутизатора.

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

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

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

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

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

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

Планируется создать метод кластеризации графа социальной сети. Для тестирования будущего метода возникла необходимость в генерации графа, по своей структуре схожего с лежащими в основе существующих социальных сетей. В статье представлен алгоритм для распределенной генерации такого графа. Учитываются основные свойства социальной сети: степенное распределение количества сообществ для пользователей, плотные пересечения сообществ и другие. В данном алгоритме учтены проблемы, присутствующие в подобных работах других авторов, например, проблема кратных ребер при генерации. Особенностью созданного алгоритма стала реализация, зависящая от такого параметра как количество сообществ, а не от количества пользователей, как это делается в других работах. Это связано с особенностью развития структуры реальной существующей социальной сети. В работе перечислены свойства ее графа. Описана таблица, содержащая необходимые для алгоритма переменные. Составлен пошаговый алгоритм генерации. Для него определены соответствующие математические параметры. Генерация происходит распределенно с помощью фреймворка Apache Spark. Подробно описано, каким образом происходит разделение задач с помощью данного фреймворка. В алгоритме используется модель Эрдеша–Реньи для случайных графов как наиболее подходящая и достаточно простая для реализации. Основными преимуществами созданного метода являются использование малого количества ресурсов, по сравнению с другими подобными генераторами, и скорость выполнения. Быстрота достигается за счет распределенной работы и того, что при распределенной работе алгоритма в любой момент пользователи сети имеют свои уникальные номера и упорядочены по этим номерам, поэтому не требуется их сортировка. Разработанный алгоритм будет способствовать не только созданию эффективного метода кластеризации. Он может быть полезен в других областях, связанных, например, с поисковыми системами социальных сетей.

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

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

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

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

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