Preview

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

Расширенный поиск
Том 19, № 6 (2012)

Editorials

7-8 203
Аннотация
Данный выпуск представляет статьи, подготовленные на основе избранных докладов Третьего международного семинара «Семантика, спецификация и верификация программ: теория и приложения» (Third Workshop on Program Semantics, Specification and Verification: Theory and Applications, PSSV 2012) и Международной конференции «Дискретная геометрия», посвященной 100-летию А. Д. Александрова (Yaroslavl International Conference on Discrete Geometry dedicated to the centenary of A. D. Alexandrov).

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

9-20 315
Аннотация

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

21-33 756
Аннотация

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

34-44 396
Аннотация

Предложен дедуктивный подход к верификации телекоммуникационных систем, представленных на языке C. Подход основан на расширении языка C декларативными операторами и сведении верификации параллельных взаимодействующих компонент телекоммуникационных систем к раздельной верификации компонент, представленных на расширенном языке. Рассмотрен пример верификации протокола передачи данных.

45-56 476
Аннотация

Исследуется задача верификации систем реального времени (СРВ). Для описания СРВ удобно использовать диаграммы состояний UML с семантикой, определяемой иерархическими автоматами. Для верификации СРВ часто применяется средство UPPAAL, разработанное для проверки формул логики TCTL на сети временных автоматов. Основным результатом данной статьи является алгоритм трансляции иерархических автоматов в сеть временных автоматов и обоснование его корректности.

57-68 392
Аннотация

Рассматривается известный протокол скользящего окна, который обеспечивает надёжную и эффективную передачу данных по ненадёжным каналам. Формальное доказательство корректности этого протокола требует преодоления существенных трудностей, связанных с высокой степенью параллелизма, которая создаёт значительные возможности для ошибок. Здесь рассматривается версия данного протокола, основанная на выборочном повторе кадров. На языке системы верификации PVS описаны спецификация этого протокола с помощью машины состояний и его свойство безопасности. С помощью системы PVS проведено в интерактивном режиме доказательство этого свойства протокола скользящего окна.

69-78 977
Аннотация

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

В данной работе предлагается усилить классический подход к обнаружению клонов на основе анализа абстрактных синтаксических деревьев (АСД) за счет использования дополнительной информации о слайсах АСД по переменным программы. Это позволяет эффективно обнаруживать разорванные (gapped) и переплетенные (intertwined) клоны – результаты предварительных экспериментов подтверждают применимость предложенного подхода на практике.

79-91 360
Аннотация

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

92-100 272
Аннотация

Ярославская международная конференция «Дискретная геометрия», посвященная 100-летию А. Д. Александрова, была организована и проведена Международной лабораторией «Дискретная и вычислительная геометрия» им. Б. Н. Делоне с 13 по 18 августа 2012 года в Ярославском государственном университете им. П.Г. Демидова. Целью настоящей статьи является освещение основных результатов, представленных на конференции, и обсуждение ее роли в развитии дискретной и вычислительной геометрии в Ярославле. Статья публикуется в авторской редакции.

101-106 291
Аннотация

Приводится эффективное описание графов многогранников задач РАЗБИЕНИЕ НА ТРЕУГОЛЬНИКИ и ПОЛНЫЙ ДВУДОЛЬНЫЙ ПОДГРАФ. Для каждого из них устанавливается, что плотность графа, то есть его кликовое число, растет экспоненциально по размерности пространства.

107-111 308
Аннотация

Рассматриваются теоремы, являющиеся обобщениями известных следствий теоремы Хелли.

112-126 287
Аннотация

Рассматриваются постановки задач локализации узлов в триангуляциях Делоне и методы их решения. Для задачи локализации множества узлов предлагается подход, основанный на прослеживании Евклидова минимального остовного дерева триангуляции Делоне. Приводятся и доказываются оценки сложности предложенных методов в среднем и худшем случаях.

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

В статье [10] нами доказано, что любой правильный многогранник P допускает непрерывное (изометричное) складывание (или разглаживание) на плоскость. В настоящей статье мы приводим явные формулы непрерывных функций такого процесса складывания для правильного тетраэдра в R³ . Статья публикуется в авторской редакции.

137-147 263
Аннотация
Построен класс совершенных призмоидов, и доказаны некоторые их свойства, связанные со знаменитой гипотезой Калаи о минимальном числе граней выпуклого центрально-симметричного многогранника. Доказано, что многогранники Ханнера, на которых согласно гипотезе Калаи достигается минимум общего числа граней у центрально-симметричного многогранника, являются совершенными призмоидами. Также доказано, что любой совершенный призмоид аффинно эквивалентен некоторому 0/1-многограннику, полученному из куба той же размерности.
148-151 301
Аннотация
Содержится развернутый план доказательства равномерной оценки дисперсии числа гиперграней случайного многогранника в случае, если объемлющее тело — простой многогранник. Таким образом, доказана ослабленная версия результата, оставленного в [1] без доказательства. Статья публикуется в авторской редакции.
152-160 316
Аннотация

Предлагается новый алгоритм генерализации линейных картографических объектов. Основным новшеством алгоритма является автоматическая сегментация – разбиение ломаной на участки с одинаковыми свойствами. Сегментация позволяет подобрать параметры сглаживания индивидуально для каждого участка, за счет чего существенно повышается качество результата.

161-169 268
Аннотация
Известно, что для каждого симплициального многогранника P в 3-пространстве существует многочлен Q, зависящий только от комбинаторного строения многогранника и длин его ребер, такой, что объемы многогранника P и любого другого изометричного P многогранника с таким же комбинаторным строением являются корнями многочлена Q. Но этот многочлен содержит много миллионов слагаемых, и его нельзя выписать в явном виде. В работе мы указываем один класс многогранников, для которых эти многочлены можно выписать в компактной форме, верной также в пространствах постоянной кривизны любой размерности.
170-172 251
Аннотация
Дано новое доказательство формулы Эйлера для замкнутого выпуклого многогранника, расположенного в трехмерном евклидовом пространстве R³.


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


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