Preview

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

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

Editorials

7-9 197
Аннотация
Данный выпуск журнала содержит статьи, подготовленные на основе докладов Четвертого международного семинара «Семантика, спецификация и верификация программ: теория и приложения» (Fourth Workshop on Program Semantics, Specification and Verification: Theory and Applications, PSSV 2013), а также докладов Международной конференции «Геометрия, топология и приложения» (Geometry, Topology, and Applications), посвященной 70-летию Н.П. Долбилина.

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

10-21 304
Аннотация

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

22-35 397
Аннотация

В последние годы такой метод обеспечения качества программного обеспечения (ПО), как ограниченная проверка моделей (Bounded Model Checking, BMC), исследуется все более и более активно, поскольку он позволяет успешно обнаруживать как функциональные, так и нефункциональные дефекты в реальном ПО. В данной статье предлагается оригинальный подход к реализации BMC, основанный на объединении результатов нескольких последних исследований в этой области: использовании системы компиляции LLVM для разбора и трансформации исходного кода, применении SMT-решателя Z3 для проверки свойств корректности и повышения эффективности анализа за счет аппроксимаций функций. Проведенные экспериментальные исследования показывают применимость подхода к реальным проектам.

36-51 456
Аннотация

Программно-коммутируемые сети (ПКС) — это класс компьютерных телекоммуникационных сетей, появившийся несколько лет назад в стремлении упростить проектирование и повысить гибкость управления сетями за счет разделения потоков данных (пакетов) и потоков управления (сообщений и команд), циркулирующих в сетях. ПКС представляет собой распределенную систему, в которой один или несколько контроллеров управляют множеством сетевых коммутаторов, обеспечивающих продвижение пакетов по каналам сети. Функциональные возможности и порядок взаимодействия коммутаторов и контроллеров ПКС определяются протоколом OpenFlow. На основе аппарата булевых функций и дискретных преобразователей нами предложена формальная модель ПКС, введен прототип формального языка спецификаций, поставлены задачи верификации моделей ПКС и получены оценки их сложности. Для одной из задач верификации моделей ПКС описан метод ее решения, на основе которого разработано программно-инструментальное средство верификации ПКС.

52-63 697
Аннотация

Развитие проекта C-light привело к применению новых формализмов и реализации методов, которые облегчают процесс верификации С-программ. Смешанная аксиоматическая семантика предлагает выбор между упрощенными и общими правилами вывода условий корректности (УК) в зависимости от программных объектов и их свойств. Инфраструктура LLVM значительно упрощает реализацию анализатора и транслятора C-light программ. Метод семантических меток, предложенный ранее, теперь может быть безопасно исполь- зован в условиях корректности при их доказательстве. Рассмотрен пример из соревнования по верификации, иллюстрирующий применение нашей системы.

64-77 440
Аннотация

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

78-94 462
Аннотация

Предлагается подход к построению и верификации LD-программ логических контроллеров (ПЛК) для «дискретных» задач. Спецификация программного поведения проводится на языке темпоральной логики линейного времени LTL. Программирование осуществляется на языке LD (Ladder Diagram) по LTL-спецификации. Анализ корректности LTL-спецификации производится с помощью программного средства символьной проверки модели Cadence SMV. Подход к программированию и верификации LD-программ ПЛК демонстрируется на примере. Для дискретной задачи приводятся LD-программа, ее LTL-спецификация и SMV-модель. Целью статьи является описание подхода к программированию ПЛК, который бы обеспечивал возможность анализа корректности LD-программ ПЛК с помощью метода проверки модели. Поэтому изменение значения каждой программной переменной описывается с помощью пары LTL-формул. Первая LTL-формула описывает ситуации, при которых происходит возрастание значения соответствующей переменной, вторая LTL-формула задает условия, приводящие к уменьшению значения переменной. Рассматриваемые для спецификации поведения переменных LTL- формулы являются конструктивными в том смысле, что по ним производится построение ПЛК-программы, которая соответствует темпоральным свойствам, выраженным этими формулами. Таким образом, программирование ПЛК сводится к построению LTL-спецификации поведения каждой программной переменной. Кроме этого, по LTL-спецификации строится SMV-модель LD-программы ПЛК, которая затем проверяется на корректность (относительно дополнительных общепрограммных LTL-свойств) методом проверки модели с помощью средства верификации Cadence SMV.

95-102 303
Аннотация

Международная конференция “Геометрия, топология и приложения”, посвященная приближающемуся семидесятилетию Николая Петровича Долбилина, была организована Международной лабораторией имени Б. Делоне “Дискретная и вычислительная геометрия” и прошла с 23 по 27 сентября 2013 года в Ярославском государственном университете им. П.Г. Демидова. Цель настоящей заметки — отметить основные результаты, представленные на конференции и подчеркнуть роль подобных мероприятий в развитии дискретной и вычислительной геометрии в России.

Статья публикуется в авторской редакции.

103-110 288
Аннотация

В статье рассматриваются ранги правильных полигональных комплексов и устанавливается, что ранги таких комплексов в E³ не могут превышать 4 и в E³ имеется только восемь правильных полигональных комплексов ранга 4. Статья публикуется в авторской редакции.

111-120 432
Аннотация
Персистентные гомологии используются для исследования топологических свойств облаков точек и функций. Рассматривая различные масштабы одновременно, можно фиксировать рождение и исчезновение топологических особенностей при изменении масштаба. В данной работе мы используем статистический метод, называемый эмпирическим бутстрэпом, для отделения топологического сигнала от топологического шума. В частности, мы получаем доверительные множества для диаграмм персистентности и доверительные интервалы для ландшафтов персистентности. Статья публикуется в авторской редакции.
121-128 279
Аннотация

Для конечной группы Кокстера W, комплекс подслов – это симплициальный комплекс, задаваемый парой (Q, ρ), где Q – слово в алфавите простых отражений, ρ – элемент группы. Мы описываем преобразования такого комплекса, индуцированные ниль-движениями и обратными операциями на Q в ниль-моноиде Гекке, соответствующем W. Если комплекс многогранен, мы также описываем эти преобразования для двойственного ему многогранника. Для просто вложенной группы W эти описания вместе с результатами [5] дают алгоритм построения комплекса подслов, соответствующего (Q, ρ) из комплекса, соответствующего (δ(Q), ρ), для любой последовательности элементарных движений, редуцирующей слово Q в его произведение Демазюра δ(Q). Первый комплекс сферичен или пуст тогда и только тогда, когда второй является пустым комплексом. Статья публикуется в авторской редакции.

129-134 305
Аннотация
Любой выпуклый многогранник P = P(α) может быть описан системой линейных неравенств, определяемых векторами p и правыми частями α(p). Для фиксированного множества векторов p определяется область типа D(P₀) многогранника P₀, и в частности параллелоэдра P₀, как такое множество параметров α(p), что много- гранники P(α) имеют тот же комбинаторный тип, что и P₀ для всех α ∈ D(P₀). Во второй части статьи дается фасетное описание зонотопов и зонотопных параллелоэдров. Статья публикуется в авторской редакции.
135-141 230
Аннотация
Мы вводим новый класс случайных упаковок, который называется “региональные случайные упаковки”. После компьютерных симуляций, с помощью статистического анализа нами получена плотность региональных случайных упаковок. Также мы исследуем одномерный случай региональных случайных упаковок. Приведены некоторые замечания о связи случайных упаковок дисков с другими процессами. Статья публикуется в авторской редакции.
142-148 305
Аннотация
Рассматривается группа гомологий пространства W˜₁(∇N ) триангуляций двумерного симплекса D₀D₁D₂с не более чем 6 точками разбиения границы в случае, когда триангуляции с границы продолжаются на внутренность симплекса без добавления новых точек разбиения. В результате получены группы гомологий Hn для n = 0, . . . , 5. Статья публикуется в авторской редакции.
149-161 321
Аннотация

Мы предлагаем один новый подход к проблеме вычисления объемов тел в пространстве Лобачевского и применяем его к тетраэдру. Используя некоторые интегральные соотношения, мы даем явные формулы для объема тетраэдра в функции координат его вершин, а также длин его ребер. Наконец, мы даем в случае тетраэдра прямое аналитическое доказательство знаменитой формулы Шлефли.

162-173 428
Аннотация

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

174-178 302
Аннотация

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

179-199 376
Аннотация

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



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


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