Оригинальные статьи 
Пусть G – конечная неединичная группа с неприводимым комплексным характером χ степени d. Согласно соотношениям ортогональности для неприводимых характеров, сумма квадратов степеней этих характеров равна порядку группы G. Н. Снайдером доказано, что если |G| = d(d + e), то порядок группы G ограничен функцией e при e > 1. Я. Берковичем доказано, что в случае e = 1 группа G является группой Фробениуса с дополнением порядка d. В данной работе изучается конечная неединичная группа G, обладающая неприводимым комплексным характером Θ, для которого |G| ≤ 2Θ(1)2. Доказано, что в случае, когда Θ(1) – произведение двух различных простых чисел p и q, группа G является разрешимой группой с абелевой нормальной подгруппой K индекса pq. С помощью классификации простых конечных групп доказано, что простая неабелева группа, порядок которой делится на простое число p и не превышает 2p4, изоморфна одной из следующих групп: L2(q), L3(q), U3(q), Sz(8), A7, M11, J1.
В данной статье рассмотрены принципы организации беспроводных mesh-сетей программно-конфигурируемых сетей подвижных объектов. Основное внимание уделяется вопросам построения эффективных алгоритмов маршрутизации для подобных сетей. Математической моделью системы является стандартная транспортная сеть. В качестве ключевого параметра системы маршрутизации рассматривается коэффициент доступности узла функция, зависящая от ряда основных и дополнительных параметров ((mesh-факторовв), характеризующих маршрут между двумя узлами сети. Каждой паре (дуга, узел) сопоставляется композитный параметр, характеризующий 裂доступностьь узла по маршруту, начинающемуся данной дугой. Лучшим ((кратчайшимм) маршрутом между двумя узлами считается маршрут с наибольшим коэффициентом доступности. Описаны правила построения и обновления таблиц маршрутизации узлами сети. Получая анонс от соседа, узел имеет сведения об энергетике соединения, надежности соединения, времени
получения анонса, отсутствии промежуточных узлов, а также располагаемой пропускной способности. На основании этой информации ко всем маршрутам, проходящим через данного соседа, может быть применена пенализация (наложение штрафа) или поощрение (увеличение коэффициента доступности). Указанная схема пенализации / поощрения складывается из отдельных аспектов:
1. Пенализация за актуальность информации.
2. Пенализация / вознаграждение за надежность узла.
3. Пенализация за энергетику соединения.
4. Пенализация за располагаемую пропускную способность.
На основе предложенных эвристических алгоритмов маршрутизации построен симулятор беспроводной mesh-сети подвижных объектов, описание и характеристики которого приведены в статье. Также рассмотрены особенности программной реализации симулятора.
В данной работе рассматривается с формальной точки зрения метод построения сетей Петри,
имитирующих поведение императивных программ. Примеры сетей Петри с заданными характеристиками являются необходимыми в процессе программирования новых алгоритмов анализа моделей программ, в частности, они могут использоваться для разработки и оптимизации алгоритмов композиции и декомпозиции сетей Петри, построения дерева достижимости, проверки инвариантов и т.д. Способ построения состоит из двух стадий. На первой стадии описываются шаблонные конструкции, из которых будет состоять результирующая сеть, и параметры, с которыми будет выполняться построение. С помощью этих параметров можно регулировать конечный размер, а также абсолютное или относительное количество определённых конcтрукций в результирующей сети. На второй стадии с помощью автоматического итерационного процесса может быть сгенерирована сеть Петри любого размера, ограниченного оперативной памятью компьютера. В первом разделе статьи приводится необходимый минимум определений и вводится новый вариант операции композиции сетей Петри по местам. Свойства коммутативности и ассоциативности бинарного вида предложенной операции позволяют сливать несколько сетей Петри в произвольном порядке. Далее вводится понятие шаблонной конструкции в виде маркированной сети Петри, обладающей входным и выходным интерфейсами, а также правилами композиции шаблонных конструкций с использованием этих интерфейсов. Множество шаблонных конструкций объединяются в набор, для которого определяются правила эволюции. Свойство полноты набора гарантирует, что в результате эволюции набора будет получена сеть Петри, имитирующая поведение императивной программы. В статье приводится вариант полного набора шаблонных конструкций и пример генерации сети Петри, имитирующей последовательную императивную программу.
В связи с увеличением сложности программного обеспечения корректность программы всё
чаще доказывается с помощью методов формальной верификации. Дедуктивный анализ на основе исчисления Хоара применим для произвольных языков программирования и допускает частичную автоматизацию процесса. Однако дедуктивный анализ не нашёл широкого применения для верификации параллельных программ из-за высокой сложности процесса. Использование функционально-потоковой парадигмы параллельного программирования позволяет снизить сложность доказательства. В работе рассматривается процесс доказательства корректности функционально-потоковых параллельных программ на языке Пифагор и предлагается архитектура инструментального средства для поддержки процесса доказательства. Процесс доказательства корректности программы представляется в виде дерева, каждый узел которого — информационный граф программы, в котором дуги размечены формулами на языке спецификации. Корнем дерева является информационный граф программы с предусловием и постусловием, которые описывают ограничения на входные переменные и условия корректности результата работы программы соответственно. Основные преобразования, применимые к информационному графу программы: разметка дуг, эквивалентное преобразование, расщепление, свертка программы. Посредством данных преобразований информационный граф модифицируется и, в конечном счете, сводится к набору формул на языке спецификации, истинность которых будет свидетельствовать о корректности программы. Предложена архитектура системы поддержки процесса доказательства, которая позволяет строить дерево доказательства. В системе выделено несколько основных модулей: «Модуль доказательства корректности программы», «Система управления библиотекой аксиом и теорем» и «Модуль анализа ошибок и выдачи информации об ошибках». Согласно описанной архитектуре, разработано инструментальное средство для поддержки формальной верификации, которая позволяет строить дерево доказательства. Описана основная функциональность реализации системы.
ISSN 2313-5417 (Online)