Развитие методов композиционального поведенческого анализа распределенных систем с мобильными агентами.

Номер гранта:16-37-00482
Область научного знания:инфокоммуникационные технологии и вычислительные системы
Тип конкурса: («мол_а»)(«мол_а») конкурс научных проектов, выполняемых молодыми учеными
Год выполнения:2016г.
Руководитель: Дворянский ЛеонидВладимирович
Статус заявки:поддержана

Аннотация к заявке:

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

Аннотация к отчету по результатам реализации проекта:

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

Библиография

Приведена в авторской редакции.
Помог ли вам материал?
0    0