Preview

Моделирование и анализ информационных систем

Расширенный поиск
Том 22, № 4 (2015)
Скачать выпуск PDF

Оригинальные статьи 

483-499 900
Аннотация

Пусть 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.

546-562 980
Аннотация

В данной статье рассмотрены принципы организации беспроводных mesh-сетей  программно-конфигурируемых сетей подвижных объектов. Основное внимание уделяется вопросам построения эффективных алгоритмов маршрутизации для подобных сетей. Математической моделью системы является стандартная транспортная сеть. В качестве ключевого параметра системы маршрутизации рассматривается коэффициент доступности узла  функция, зависящая от ряда основных и дополнительных параметров ((mesh-факторовв), характеризующих маршрут между двумя узлами сети. Каждой паре (дуга, узел) сопоставляется композитный параметр, характеризующий 裂доступностьь узла по маршруту, начинающемуся данной дугой. Лучшим ((кратчайшимм) маршрутом между двумя узлами считается маршрут с наибольшим коэффициентом доступности. Описаны правила построения и обновления таблиц маршрутизации узлами сети. Получая анонс от соседа, узел имеет сведения об энергетике соединения, надежности соединения, времени
получения анонса, отсутствии промежуточных узлов, а также располагаемой пропускной способности. На основании этой информации ко всем маршрутам, проходящим через данного соседа, может быть применена пенализация (наложение штрафа) или поощрение (увеличение коэффициента доступности). Указанная схема пенализации / поощрения складывается из отдельных аспектов:
1. Пенализация за актуальность информации.
2. Пенализация / вознаграждение за надежность узла.
3. Пенализация за энергетику соединения.
4. Пенализация за располагаемую пропускную способность.
На основе предложенных эвристических алгоритмов маршрутизации построен симулятор беспроводной mesh-сети подвижных объектов, описание и характеристики которого приведены в статье. Также рассмотрены особенности программной реализации симулятора.

563-577 1080
Аннотация

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

578-589 1102
Аннотация

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



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


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)