Существенная часть программного обеспечения написана на языках программирования C/C++. Программы на этих языках часто содержат ошибки: использования памяти после освобождения (Use After Free, UAF), переполнения буфера (Buffer Overflow) и др. В статье предложен метод обнаружения ошибок UAF, основанный на динамическом анализе. Для каждого пути выполнения программы предлагаемый метод проверяет корректность операций создания и доступа, а также освобождения динамической памяти. Поскольку применяется динамический анализ, поиск ошибок производится только в той части кода, которая была непосредственно выполнена. Используется символьное исполнение программы с применением решателей SMT (Satisfiability Modulo Theories) [12]. Это позволяет сгенерировать данные, обработка которых приводит к обнаружению нового пути выполнения.

В последние десятилетия переполнение буфера остаётся одним из главных источников программных ошибок и эксплуатируемых уязвимостей. Среди прочих подходов к устранению подобных дефектов активное развитие получили различные методы статического анализа. В работе рассматриваются основные подходы и инструменты, используемые для решения этой задачи, с целью выявить наиболее популярные методы и типы обнаруживаемых ошибок. Также исследованы наборы синтетических тестов (Juliet Test Suite, Toyota ITC benchmark) и выборка фрагментов кода реальных приложений, содержащих эксплуатируемую ошибку переполнения буфера. Для понимания направлений развития промышленного статического анализатора важно рассматривать оба эти источника примеров ошибочных программ. Наборы тестов очерчивают круг ситуаций, которые необходимо поддержать в анализаторе, при этом их легко понять, классифицировать и проверить. С другой стороны, они не отражают распределение таких ситуаций в реальном коде. Выборка уязвимостей из промышленных проектов также представляет интерес для исследования, но оказывается смещённой в сторону эксплуатируемых ошибок и к тому же не включает ошибки, исправленные на стадии разработки (возможно, как раз с использованием статического анализатора). Полученные данные были использованы для выделения основных шаблонов дефектов, которые должен обнаруживать статической анализатор с точки зрения пользователя. В результате исследования к наиболее важным возможностям статического анализатора были отнесены межпроцедурный путе- и контекстно-чувствительный анализ, а также базовая поддержка циклов. Кроме того, полезными оказываются отслеживание аффинных отношений между переменными и моделирование строк как важного случая использования массивов. Результаты данного исследования используются для улучшения детектора переполнения буфера, реализованного в рамках инфраструктуры статического анализатора Svace. На данный момент используется межпроцедурный чувствительный к путям и контексту анализ, позволяющий обнаруживать переполнения буфера на стеке и в статической памяти с долей истинных срабатываний 65%. По результатам исследования наиболее перспективными направлениями представляются поддержка строковых операций и внедрение анализа помеченных данных в имеющиеся подходы.

Модельно-ориентированный подход к разработке позволяет построить архитектурную модель существующей системы по ее исходному коду. Построенная архитектурная модель существующей системы позволяет проанализировать ее различные статические и динамические характеристики, включая производительность, требуемые аппаратные ресурсы, надежность и другие. Архитектурные модели могут использоваться как для анализа, так и для повторного использования некоторых компонентов существующей системы в новом проекте. Во многих случаях такой подход позволяет избежать построения новой системы с нуля. Для создания архитектурных моделей могут использоваться различные языки моделирования. В данной работе используется язык анализа и проектирования архитектуры (AADL). Данная статья описывает алгоритм извлечения архитектурной информации из исходного кода ARINC 653 совместимых программных приложений. Спецификация ARINC 653 определяет требования к программным компонентам для систем интегрированной модульной авионики (ИМА). Для доступа к различным сервисам операционной системы программные приложения используют прикладной исполняемый интерфейс. Архитектурная информация в исходном коде программных приложений совместимых с требованиями спецификации ARINC 653 включает процессы в каждом разделе, объекты для взаимодействия между процессами внутри и за пределами раздела, а также глобальные переменные. Для анализа исходного кода и получения архитектурной информации необходимо проанализировать все программные вызовы прикладного исполняемого интерфейса. Извлеченная архитектурная информация далее используется для построения архитектурных моделей системы. Для анализа исходного кода используется подход на основе алгоритма CEGAR (уточнение абстракции с помощью контрпримера), широко используемого при верификации программного обеспечения. Алгоритм CEGAR анализирует возможные пути исполнения программы, используя представление программы в виде абстрактного графа достижимости. В классическом алгоритме CEGAR исследуемый путь программы называется контрпримером и означает путь от начала программы до некоторого ошибочного состояния. Для подтверждения наличия ошибки в коде программы алгоритм CEGAR выполняет проверку достижимости для исследуемого пути. В программном инструменте CPAchecker базовый основанный на предикатах алгоритм CEGAR расширен для анализа явных значений переменных. В данной статье расширенный для анализа явных значений переменных алгоритм CEGAR используется для задачи извлечения архитектурной информации из исходного кода приложений. Основной вклад данной статьи заключается в применении идей контрпримера и проверки достижимости пути к задаче извлечения архитектурной информации из исходного кода приложений.

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

Большая часть стандартных для программирования задач - например, соединение с базой данных, отображение картинки, чтение файла - давно реализована в различных библиотеках и доступна через соответствующие Application Programming Interfaces (APIs). Однако чтобы воспользоваться ими, разработчик должен сначала узнать, что они существуют, а затем - как правильно с ними работать. В настоящее время Интернет кажется наилучшим и самым популярным источником подобной информации. Недавно был предложен другой подход, основанный на глубоком машинном обучении и реализованный в виде инструмента под названием DeepAPI. По описанию желаемой функциональности на английском языке он генерирует цепочку вызовов Java функций. В данной статье мы показываем, как подход может быть перенесен на другой язык программирования (C# вместо Java), на котором доступно меньше открытого кода; мы описываем техники, позволившие достичь результата, близкого к оригинальному, а также техники, которые не улучшили производительность. Наконец, чтобы облегчить будущие исследования в области, мы публикуем наши набор данных, код и обученную модель.

При анализе программ на наличие уязвимостей и вредоносного кода бывают ситуации, в которых возникает необходимость качественной изоляции инструментов анализа. Этому есть две причины. Во-первых, анализируемая программа может влиять на инструментальную среду. Эта проблема решается использованием эмулятора. Во-вторых, инструменты анализа могут влиять на программу. Так, программист может подумать, что программа безопасна, хотя на самом деле это может быть не так. Эта проблема может быть решена механизмом скрытой отладки. Отладчик WinDbg имеет функцию подключения к удаленному отладочному серверу (Kdsrv.exe), запущенному в ядре Windows. Поэтому есть возможность подключиться к гостевой системе, запущенной в эмуляторе QEMU. Клиент взаимодействует с сервером через пакеты по протоколу KDCOM. Однако отлаживать ядро можно лишь с включенным режимом отладки в настройках запуска, что раскрывает процесс отладки. Мы разработали специальный модуль отладчика WinDbg для QEMU, который является альтернативой удаленному отладочному сервису в ядре. Модуль перехватывает пакеты при взаимодействии клиента отладчика WinDbg с сервером, самостоятельно генерирует всю необходимую отладочную информацию, используя возможности эмулятора Qemu, и отправляет ответ клиенту. Модуль полностью эмулирует поведение отладочного сервера, поэтому клиент на замечает подмены и успешно взаимодействует с ним. При этом отпадает необходимость в отладочном режиме ядра. Тем самым происходит скрытая отладка. При использовании модуля работоспособны все возможности WinDbg, которые он представляет для удаленной отладки, кроме перехвата событий и исключений.

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

Проводится анализ моделей и методов оценки надежности технических и программных средств. Определяются основные понятия методов надежности и безопасности таких систем и ситуаций, приводящих к ошибкам, дефектам и отказам. Дано определение надежности и безопасности технических систем и программного обеспечения (ПО) систем. Приведена классификация моделей надежности: прогнозирующего, измерительного и оценочного типов. Описаны оценочные модели, которые применяются на практике. Определен стандарт жизненного цикла ПО (ISO 15288:2002), ориентированный на разработку и контроль компонентов систем на ошибки, начиная с требований к системе. Представлены результаты применения моделей надежности (Мусы, Гоэла-Окомото и др.) к малым, средним и большим проектам и дана сравнительная их оценка. Описан технологический модуль (ТМ) оценки надежности сложных комплексов программ ВПК (1989). Показана модель качества стандарта ISO 9126 (1-4):2002-2004 с показателями функциональность, надежность, эффективность и др., которые используются при определении зрелости и сертификата качества продукта.

Необходимость эмуляции оборудования часто возникает на различных стадиях цикла разработки, миграции оборудования или обратной разработки. Реализация алгоритмов, связанных с конкретным устройством, сама по себе является нетривиальной задачей, но интеграция эмулятора с существующей средой, например, драйверами, предназначенными для работы с реальным оборудованием, зачастую оказывается не менее сложной. Устройства, полагающиеся на ввод-вывод с отображением в оперативную память, представляют особый интерес, так как в этих случаях, в отличие от использования портов ввода-вывода, гораздо меньше вероятность, что целевая платформа предоставит интерфейс для перехвата операций. Один из распространённых подходов, широко используемый в ПО виртуальных машин, состоит в том, чтобы поместить всю операционную систему под гипервизор и создать внешний эмулятор. Однако это может быть нежелательно по причинам сложности гипервизора, потери производительности, дополнительных требований к аппаратному обеспечению и пр. В данной статье такой подход распространяется на ядро, и предлагается описание возможности построить эмулятор, прибегая лишь к существующим интерфейсам, предоставляемым операционной системой. Ввиду частой доступности MMU и механизмов защиты страниц, позволяющих перехватывать доступ записи и чтения, предполагается, что предлагаемый подход может быть использован на значительном количестве целевых платформ. В статье приводится подробное рассмотрение проблем, возникающих при написании конкретной реализации, и приводятся способы её упрощения и оптимизации в зависимости от возможностей целевой платформы, эмулируемого протокола и иных требований к задаче. В качестве экспериментального доказательства работоспособности предлагаемого подхода приводится реализация эмулятора SMC для платформы x86.

Современные операционные системы реального времени являются сложным продуктом, разрабатываемым многими поставщиками: непосредственными разработчиками ОС, поставщиками пакета поддержки аппаратуры, разработчиками драйверов устройств и т.д. Такие ОС спроектированы так, чтобы иметь возможность запускаться на различном оборудовании, часто имеющем ограниченные ресурсы. Встраиваемые ОС содержат множество настроек и драйверов для поддержки разной аппаратуры. Большинство из этих драйверов являются излишними для запуска ОС на каком-то конкретном оборудовании. ОС статически конфигурируется для выбора набора драйверов и настроек для каждого типа аппаратуры. Модульность ОС упрощает как разработку ОС, так и ее конфигурирование. Разделение ОС на изолированные модули с фиксированными интерфейсами уменьшает необходимость взаимодействия между разработчиками в ходе совместной разработки. Мы используем формальные модели для описания компонентов и их взаимодействия. Использование формальных моделей приносит большую пользу. Описываемые модели содержат достаточно информации для генерации исходного кода компонента на языке Си. Предоставляемые модели являются исполняемыми, что позволяет человеку, отвечающему за конфигурацию, быстро проверить правильность заданной конфигурации. Кроме того, модель содержит ограничения на конфигурационные параметры. Примером таких ограничений являются ограничения на внутреннюю согласованность модели. При генерации исходного кода такие ограничения транслируются в специальные проверки на уровне исходного кода. Следовательно, ограничениями могут быть проверены как во время симуляции модели, так и во время исполнения исходного кода. В данной работе представлен подход к описанию таких моделей на языке программирования Scala. Мы успешно апробировали данный подход на основе ОС реального времени JetOS.

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

Хорошая спецификация криптографического протокола должна легко восприниматься человеком (быть декларативной и лаконичной), быть исполнимой и пройти процедуру формальной верификации в некоторой адекватной модели. Нацеливаясь на эти требования, в статье предложена нотация CMN.1, предназначенная для описания сообщений криптографических протоколов и основанная на вычислительной абстракции под названием криптографическая стековая машина (CSM). Статья описывает синтаксис и семантику CMN.1, а также представляет результаты разработки языка спецификаций криптографических протоколов, построенного на основе данной нотации и встроенного в язык Haskell. В авторской реализации вся обработка сообщений инкапсулирована внутри базового библиотечного модуля, в то время как спецификация должна лишь дать декларативные определения этих сообщений. При формировании исходящего сообщения протокола базовый модуль берет описание данного сообщения в нотации CMN.1 и возвращает фрагмент данных, сгенерированный по этому описанию. При обработке входящего сообщения базовый модуль берет поступивший фрагмент данных и описание ожидаемого сообщения в нотации CMN.1 и возвращает вердикт об их соответствии друг другу, извлекая и запоминая при этом все содержащиеся в сообщении данные, необходимые для формирования или верификации следующих сообщений протокола. Процесс верификации является полным: базовый модуль осуществляет расшифрование, проверку кодов аутентификации сообщений и значений цифровой подписи и т.д. Текущая реализация языка включает функции трансляции спецификаций в исполняемый код, совместимый с существующими программными реализациями протоколов, а также функции конвертации спецификаций в программы на входном языке анализатора протоколов ProVerif. В качестве иллюстрации приводятся выдержки из CMN.1-спецификации протокола TLS и соответствующей ей автоматически сгенерированной программы для ProVerif.

В статье предложены подходы к функциональной верификации контроллеров сопряжения интерфейсов в составе микропроцессоров на основе разработки многоуровневых тестовых-систем по методологии UVM. В современных микропроцессорных системах существует множество контроллеров, работающих с собственными типами данных. Контроллеры сопряжения интерфейсов учувствуют в передаче и преобразовании данных между блоками микропроцессора. Такое преобразование должно осуществляться быстро и без повреждения данных для корректного функционирования всей системы. Контроллеры сопряжения интерфейсов могут выполнять дополнительные функции, такие как передача значений копий системных регистров, преобразование адресов и другие. В статье дан краткий обзор средств верификации и преимуществ применения автономной имитационной верификации для проверки корректности контроллеров сопряжения интерфейсов в составе подсистем связи. Представлены подходы к построению автономной верификационной тестовой системы на основе методологии UVM с модулем проверки, реализованным во внешней функциональной эталонной модели. Так же предложены методы проверки корректности подсистем связи: проверка контроллеров, работающих с несколькими синхросигналами при помощи параметризованного генератора синхросигналов, поддержка механизмов обмена кредитами. Представленные подходы использованы для верификации подсистемы связи - Host-Bridge - восьмиядерного микропроцессора с архитектурой Sparc V9, разработанного компанией АО «МЦСТ». В статье описаны проблемы, обнаруженные в процессе разработки тестовой системы и способы их разрешения. Представлены результаты использования рассмотренных решений для верификации контроллеров подсистем связи и дальнейший план совершенствования тестовой системы.

В статье описаны подходы, которые использовались для верификации контроллеров связи в системах на кристалле, разрабатываемых в МЦСТ. Представлен список контроллеров связи, а также их характеристики. Приведены принципы работы контроллеров на уровне транзакций, канальном и физическом, и отмечен их общий функционал. Затем описан общий подход к верификации устройств: принцип проектирования тестовой системы, генерации случайных тестовых воздействий и проверки поведения устройства. Представлена общая структура тестовой системы, основанная на общих свойствах устройств. Она включает компоненты для работы с интерфейсом уровня транзакций (системный агент, реализующий коммуникационный протокол системы на кристалле), интерфейсом физического уровня (физический агент, реализующий коммуникационный протокол между различными системами на кристалле на одной плате), модуль конфигурационного интерфейса, определяющего режим работы устройства, а также модуль проверки. Отмечено, что поскольку устройства исполняют только преобразования транзакций между различными представлениями, заключение о корректности поведения осуществляется на основании простой проверки совпадения входящих и исходящих транзакций. Кроме того, приведены особенности функционала устройств, которые требуют адаптации общего подхода. Объяснено, как верификация данных особенностей работы устройств определила детали структуры тестовых систем. Описано, как замена физического агента на второй контроллер связи позволяет ускорить разработку тестовой системы. Представлены методы и сложности верификации конечного автомата тренировки и состояния линка (LTSSM). Описана структура и принцип работы системных агентов, поддерживающих прямой доступ к памяти (DMA). В заключение приведен список найденных ошибок и направления дальнейшей работы.

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

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

Задача маршрутизации является одной из важнейших NP-трудных задач комбинаторной оптимизации. Она заключается в нахождении множества оптимальных замкнутых маршрутов с целью развозки товаров клиентам, используя ограниченное количество транспортных средств. В данной работе анализируется особый вид задачи маршрутизации - задача маршрутизации с ограничением по грузоподъемности, в которой у каждого транспортного средства есть лимит на максимальный вес (объем) груза. Целью данной работы является составление классификации различных типов задачи маршрутизации с ограничением по грузоподъемности. В первой части работы дана общая информация о проблеме, указаны рамки, в которых проводилось исследование - не рассматривались динамические и стохастические подвиды задачи маршрутизации. Во второй части представлена впервые предложенная авторами работы математическая постановка трех классических вариантов задачи маршрутизации с ограничением по грузоподъемности. В третьей части работы представлен список подклассов рассматриваемой задачи, включающий описание, математические модели для некоторых задач, а также наиболее перспективные метаэвристики, с помощью которых можно решать поставленную задачу. В четвертой части приведено упоминание об алгоритме LKH-3, способном решать некоторые подклассы задач с меньшим отклонением от оптимального значения по сравнению с другими алгоритмами. В заключении, приведена таблица, объединяющая все методы, описанные ранее, и схема с взаимосвязями задачи маршрутизации с ограничением по грузоподъемности и её подклассами. В будущем авторы работы планируют расширить классификацию, включив в неё подклассы стохастических и динамических вариантов данной проблемы.

В этой статье представлены результаты применения различных методов системного анализа (CATWOE, Rich Picture, AHP, Fuzzy AHP) для оценки учебных ассистентов для преподавателей. В статье рассмотрено применение soft- и hard-методов системного анализа. Методы системного анализа рассматриваются на примере реализации программы «Учебный ассистент» в Национальном Исследовательском Университете «Высшая школа экономики» (НИУ ВШЭ) на дисциплине «Дискретная математика». В статье показан процесс взаимодействия преподавателей с учениками и преподавателями в форме Rich Picture. Определены связующие мероприятия, встречи и даже отчеты, которые предоставляют ассистенты преподавателю. Затем описано каким образом были выбраны критерии для оценки ассистентов и оценена важность каждого критерия. Были определены три группы критериев: профессиональные навыки, навыки общения, личные качества. Каждая группа имеет некоторые подкритерий, которые были определены посредством уточняющих встреч и мозгового штурма. Также в работе был определен собственный метод оценки, который явился пререквизитом для AHP и позволивший сразу же отбросить наиболее неперспективных ассистентов. Кроме того, рассматривается применение методов AHP и Fuzzy AHP типа 2 для оценки учебных ассистентов. Выявлены сильные и слабые стороны каждого метода. Также показано, что, несмотря на мощь методов системного анализа, необходимо использовать здравый смысл и логику. Нельзя полагаться только на числа, полученные методами системного анализа, необходимо затем производить анализ результатов. В процессе работы выбирается лучший учебный ассистент, и определяется группа лучших учебных ассистентов.

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

В работе предложен подход для моделирования и симуляции поведения мультиагентных систем (МАС) с применением сетей Петри. МАС представляется как конечное множество сетей потоков работ. Асинхронные взаимодействия агентов описываются с помощью интерфейса, который определяется логической формулой над множеством атомарных ограничений. Эти ограничения задают порядок выполнения внутренних действий агентов. В статье рассматриваются только ациклические взаимодействия агентов. Также был разработан алгоритм симуляции поведения МАС с учетом ограничений взаимодействия агентов. Алгоритм реализован в виде подключаемого модуля для инструмента ProM 6. Предложенный подход может быть использован для оценки качества алгоритмов извлечения процессов (process discovery) с точки зрения характеристик получаемых моделей процессов.

Последовательные реагирующие системы - это программы, которые взаимодействуют с окружением, получая от него сигналы или запросы, и реагируют на эти запросы, проводя операции с данными. Подобные системы могут служить моделью для многих программ: драйверов, систем реального времени, сетевых протоколов и др. В статье исследуются задача верификации программ такого вида. В качестве формальных моделей для реагирующих систем мы используем конечные автоматы-преобразователи, работающие над полугруппами. Для описания поведения автоматов-преобразователей введён новый язык спецификаций LP-CTL*. В его основу положена темпоральная логика CTL*. Этот язык спецификаций имеет две характерные особенности: 1) каждый темпоральный оператор снабжён регулярным выражением над входным алфавитом автомата, и 2) каждое атомарное высказывание задается регулярным выражением над выходным алфавитом автомата-преобразователя. В данной работе представлен табличный алгоритм проверки выполнимости формул LP-CTL* на моделях конечных автоматов-преобразователей, работающих над свободными полугруппами. Доказана корректность предложенного алгоритма и получена оценка его сложности. Кроме того, рассмотрен специальный фрагмент языка LP-CTL*, содержащий в качестве параметров темпоральных операторов только регулярные выражения над однобуквенным алфавитом. Показано, что этот фрагмента применим для спецификаций обычных моделей Крипке, и при этом его выразительные возможности превосходят обычную логику CTL*.

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

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