Editorials 
Оригинальные статьи
Одной из самых сложных проблем при статическом анализе программ является анализ вызовов функций, также известный как межпроцедурный анализ. Классическим способом решения этой проблемы является подстановка тел функций в места вызовов, однако при этом значительно возрастает вычислительная сложность анализа из-за увеличения размера модели программы. Для решения этой проблемы можно использовать различные алгоритмы аппроксимации функций, которые заменяют полное тело функции на ее упрощенное описание, тем самым снижая сложность анализа. В контексте ограниченной проверки моделей в последнее время начала активно использоваться интерполяция Крейга, однако ее использование возможно только для пары несовместных логических формул.
В данной статье предлагается подход к аппроксимации функций, основанный на интерполяции Крейга, который лишен данного ограничения за счет усиления интерполяции при помощи случайной выборки моделей. При помощи поиска интересных взаимозависимостей между входными и выходными аргументами функции, случайная выборка моделей позволяет усилить совместные формулы до несовместных, тем самым делая возможным использование интерполяции Крейга. Результаты проведенных предварительных экспериментов подтверждают применимость данного подхода; в дальнейшем планируется провести более подробные исследования его характеристик на реальных примерах.
Работа посвящена проблеме проверки правильной организованности (бездефектности) сетей потоков работ с ресурсами. Поток работ называется бездефектным, если он может быть корректно завершен от любого достижимого состояния. Рассматривается класс схем ресурсно-ограниченных потоков работ (RCWF-сетей), в которых экземпляры процесса могут использовать внешние ресурсы, но не могут за время своей жизни изменить их количество.
Две бездефектные RCWF-сети, использующие один и тот же набор ресурсов, могут быть запущены параллельно. Подобная параллельная композиция в некоторых случаях может порождать дополнительные тупики, вызванные взаимными блокировками. Мы исследуем проблему обнаружения потенциальных блокировок и предлагаем способы организации такого управления сетью, которое позволило бы их избегать.
В статье представлен подход к формальной верификации алгоритмов мультиагентного анализа данных для пополнения онтологий. Агенты системы на основе входных данных устанавливают значения элементов объектов, полученных на предварительной стадии анализа. Агенты параллельно осуществляют проверку семантической и синтаксической согласованности, используя правила пополнения онтологий и обработки данных. Поскольку агенты действуют параллельно, необходимо верифицировать некоторые важные свойства системы, связанные с этим, например, свойство корректности определения завершения работы системы. В нашем подходе используется инструмент проверки моделей SPIN. Протоколы агентов записаны на языке Promela, а свойства мультиагентной системы анализа данных выражены в логике LTL. Мы провели ряд экспериментов по проверке данной модели.
В работе представлены два метода, направленных на решение задачи автоматизации отладки поведенческих сценариев приложения: полуавтоматический и автоматический. Первый дает возможность пользователю автоматизировать поиск тех мест в выбранном символьном поведенческом сценарии, в которых кроется возможная причина ошибки. Второй позволяет в едином цикле анализа автоматически идентифицировать не только места, но и возможные причины ошибок в заданном множестве сгенерированных символьных поведенческих сценариев.
Разработка алгоритмов реконфигурирования сетей является важным направлением развития программного обеспечения для телекоммуникационных сетей нового поколения — программно-конфигурируемых сетей. Частный случай проблемы реконфигурирования сетей — это задача плавного восстановления заданной сетевой конфигурации, после того как некоторые правила коммутации пакетов были удалены из таблиц коммутаторов (например, по истечении срока их активности). В данной статье проведено исследование этой задачи в рамках формальной модели программно-конфигурируемых сетей, предложены корректные и безопасные алгоритмы восстановления сетевых конфигураций и показано, что в общем случае задачу плавного восстановления конфигураций нельзя решить без обращения к правилам коммутации с приоритетами.
По сравнению с традиционным тестированием дедуктивная верификация предлагает более формальный способ доказательства корректности программ. Но как установить корректность самой системы верификации? Теоретические основы логик Хоара исследовались в классических работах, где были получены различные результаты по непротиворечивости и полноте. Однако нам не известны реализации этих теоретических методов, проверенные чем-либо отличным от обычного тестирования. Иными словами, нас интересует система верификации, которая может быть применена к самой себе (хотя бы частично). В наших исследованиях мы обратились к методу метагенерации, который выглядит многообещающим для этой задачи.
В настоящее время автоматическая генерация тестов исследуется все более и более активно, поскольку является решением многих проблем, связанных с тестированием программного обеспечния (ПО), таких как необходимость написания тестов и обеспечения тестового покрытия с учетом человеческого фактора.
Наиболее перспективным методом автоматической генерации тестов является динамическое символьное исполнение (dynamic symbolic execution, DSE), выполняемое с помощью автоматического решателя ограничений, например SMT-решателя. Данный метод во многом похож на метод ограниченной проверки моделей, который также предполагает построение моделей из исходного кода, проверку логических свойств на них и обработку полученной модели.
В данной работе рассматривается метод генерации модульных тестов для языка C, основанный на методе ограниченной проверки моделей. Показано, что эти методы имеют много общего и могут быть реализованы с использованием общих базовых компонентов. Реализован прототип средства генерации тестов, основанный на работающем средстве ограниченной проверки моделей Borealis.
Прототип средства был опробован на множестве примеров и показал хорошие результаты с точки зрения полноты тестового покрытия и избыточности тестового набора.
Стандартный язык диаграмм последовательных сообщений MSC предназначен для описания сценариев взаимодействия объектов. Благодаря своей выразительности и простоте MSC-диаграммы широко применяются на практике на всех этапах проектирования и разработки программных систем. В частности, язык MSC используется для спецификации поведения в распределенных системах и коммуникационных протоколах. В работе рассматривается метод анализа и верификации диаграмм MSC и HMSC. Метод основывается на трансляции конструкций (H)MSC в раскрашенные сети Петри. Описываемые правила трансляции охватывают большинство конструкций стандарта, включая концепцию данных. Приводятся оценки размера сетей Петри, полученных в результате трансляции. Свойства построенных сетей анализируются и верифицируются с помощью известной системы CPN Tools и системы автоматической верификации на основе SPIN. Работоспособность данного метода продемонстрирована на примере.
Как и другие программные продукты, языки моделирования развиваются со временем. В результате изменений в языке, модели на данном языке могут перестать соответствовать новой метамодели языка, что ведет к невозможности работы с ними с помощью инструментов моделирования. Таким образом, возникает проблема переноса моделей на новую версию языка. В настоящее время существуют различные подходы к решению данной проблемы – от полностью ручных до практически полностью автоматизированных. Данная статья описывает гибридный подход к миграции моделей, реализованный в DSM- платформе QReal, разрабатываемой на кафедре системного программирования Санкт-Петербургского государственного университета. Рассматриваемая система накладывает некоторые специфические требования, такие как под- держка режимов интерпретации метамодели и метамоделирования “на лету”. Представленный в статье подход реализует миграцию моделей при использовании данных возможностей.
В работе описан алгоритм выделения шаблонов переменной длины из последовательностей системных вызовов. Эти шаблоны используются для идентификации процессов – установления того, что некоторая последовательность вызовов была сгенерирована тем же самым процессом, из которого были выделены шаблоны. Существующие алгоритмы либо вычислительно сложны, либо имеют высокий уровень ложных срабатываний по сравнению со сложным и ненадежным автоматным подходом. Предложенный в работе алгоритм имеет низкую вычислительную сложность и большую точность, чем классический N-граммный алгоритм. Тесты производительности показали, что реализованный монитор системных вызовов несущественно замедляет работу операционной системы. Предложенный алгоритм после двадцатиминутного обучения способен идентифицировать за одну минуту потоки процессов с точностью 85%. Поведенческая идентификация потоков программ используется для аномального обнаружения вредоносных воздействий на систему.
Часто при разработке сложных программных систем используется более чем один язык программирования. В таком случае принято говорить об основном (или исходном) языке и одном или нескольких встроенных языках. Из строковых выражений основного языка динамически формируются программы на отличном от него языке, которые потом интерпретируются специальными, работающими во время исполнения компонентами, такими как базы данных или веб-браузеры. Большинство языков программирования общего назначения могут играть роль как основного, так и встроенного языка. Самый яркий пример реализации такого подхода — динамический SQL, специфицированный в стандарте ISO SQL и поддерживаемый большинством СУБД. Автодополнение и подсветка синтаксиса — стандартная для интерактивных сред разработки функциональность — значительно упрощают процесс разработки с использованием встроенных языков. Существует несколько инструмен- тов, предоставляющих функциональность интегрированных сред разработки для встроенных языков, но они в основном поддерживают только один конкретный встроенный язык, и поддержка другого языка требует нетривиального ручного вмешательства. Мы продемонстрируем разрабатываемую платформу, позволяющую создавать инструменты для статического анализа динамически формируемых выражений.
Статья посвящена описанию технологии, позволяющей сократить трудозатраты на создание тестов для промышленных программных проектов, за счет использования инкрементального подхода. Основная проблема, решенная в данной работе, связана с полной автоматизацией фазы дизайна тестовых сценариев и сокращением количества тестов, необходимых для обеспечения качества программного продукта. Предлагаемая в работе технология позволяет решить указанные проблемы за счет совместной работы дизайнера тестовых наборов и заказчика с использованием формальных моделей, методов символьной верификации и автоматической генерации тестовых наборов на базе использования инструментария VRS/TAT.
В данной работе представлено описание программного комплекса для хранения, анализа и визуализации графов социальных сетей. Проводится сравнительный анализ существующих программных продуктов для анализа и визуализации графов. Кроме того, представлена общая архитектура приложения, описаны принципы его построения и работы основных модулей. Отдельно приведено описание разработанного графового хранилища, ориентированного на хранение и обработку графов больших размеров. В качестве основной функциональности программного продукта представлены разработанный алгоритм выделения сообществ и реализованные алгоритмы авторазмещения графов. Преимущество разработанного программного продукта заключается в высокой скорости работы с сетями больших размеров, достигающих нескольких миллионов вершин и связей. Кроме того, используемая архитектура хранилища графов является уникальной и не имеет аналогов на данный момент. Имеющиеся в ней подходы и алгоритмы оптимизированы для работы с большими графами и обладают высокой производительностью.
В 2014 году в рамках научно-образовательного центра «Нелинейная динамика» продолжил работу научный семинар, посвященный исследованиям поведения, а также методам анализа динамических систем. В текущем году на нем было заслушано более тридцати сообщений по тематике исследований научно-образовательного центра. Доклады были посвящены численному анализу с помощью различных, в том числе гибридных, вычислительных систем, бегущих волн уравнения КПП с запаздыванием и задачи теплопроводности в сложной области с источниками, в ряде докладов строились и исследовались нормальные и квазинормальные формы дифференциальных уравнений с несколькими запаздываниями, кроме того, был сделан доклад об одной задаче оптимального управления телескопическим манипулятором.
Ниже представлены тезисы наиболее интересных докладов, прозвучавших на семинаре.
ISSN 2313-5417 (Online)
