Данный выпуск представляет статьи, подготовленные на основе избранных докладов Третьего международного семинара «Семантика, спецификация и верификация программ: теория и приложения» (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).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Содержится развернутый план доказательства равномерной оценки дисперсии числа гиперграней случайного многогранника в случае, если объемлющее тело — простой многогранник. Таким образом, доказана ослабленная версия результата, оставленного в [1] без доказательства. Статья публикуется в авторской редакции.

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

Известно, что для каждого симплициального многогранника P в 3-пространстве существует многочлен Q, зависящий только от комбинаторного строения многогранника и длин его ребер, такой, что объемы многогранника P и любого другого изометричного P многогранника с таким же комбинаторным строением являются корнями многочлена Q. Но этот многочлен содержит много миллионов слагаемых, и его нельзя выписать в явном виде. В работе мы указываем один класс многогранников, для которых эти многочлены можно выписать в компактной форме, верной также в пространствах постоянной кривизны любой размерности.

Дано новое доказательство формулы Эйлера для замкнутого выпуклого многогранника, расположенного в трехмерном евклидовом пространстве R³.