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

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

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

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

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

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

Стандартный язык диаграмм последовательных сообщений MSC предназначен для описания сценариев взаимодействия объектов. Благодаря своей выразительности и простоте MSC-диаграммы широко применяются на практике на всех этапах проектирования и разработки программных систем. В частности, язык MSC используется для спецификации поведения в распределенных системах и коммуникационных протоколах. В работе рассматривается метод анализа и верификации диаграмм MSC и HMSC. Метод основывается на трансляции конструкций (H)MSC в раскрашенные сети Петри. Описываемые правила трансляции охватывают большинство конструкций стандарта, включая концепцию данных. Приводятся оценки размера сетей Петри, полученных в результате трансляции. Свойства построенных сетей анализируются и верифицируются с помощью известной системы CPN Tools и системы автоматической верификации на основе SPIN. Работоспособность данного метода продемонстрирована на примере.

Как и другие программные продукты, языки моделирования развиваются со временем. В результате изменений в языке, модели на данном языке могут перестать соответствовать новой метамодели языка, что ведет к невозможности работы с ними с помощью инструментов моделирования. Таким образом, возникает проблема переноса моделей на новую версию языка. В настоящее время существуют различные подходы к решению данной проблемы – от полностью ручных до практически полностью автоматизированных. Данная статья описывает гибридный подход к миграции моделей, реализованный в DSM- платформе QReal, разрабатываемой на кафедре системного программирования Санкт-Петербургского государственного университета. Рассматриваемая система накладывает некоторые специфические требования, такие как под- держка режимов интерпретации метамодели и метамоделирования “на лету”. Представленный в статье подход реализует миграцию моделей при использовании данных возможностей.

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

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

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

Представлена новая система, ориентированная на создание специализированных баз данных и систем управления базами данными. На основе анализа ряда NoSQL решений были выработаны принципы создания такой системы. В статье излагаются основные особенности примененного подхода, которые заключаются в том, что: а) предоставляются гибкие средства типовых определений, позволяющие создавать схемы структуризации данных, соответствующие разным парадигмам; б) сформирована система различных форм поддержания структурных значений и их отображений в файловые представления. Были проведены эксперименты с реализацией графов RDF, связанных реляционных таблиц, таблиц имен, объектно-реляционных отображений. Подход позволяет решать некоторые задачи создания технологий работы с большими данными.

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

Ниже представлены тезисы наиболее интересных докладов, прозвучавших на семинаре.