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

Видео "мультиагентные системы"
//PROBOTICS PHASE 01 //AADRL 2008/2009
//Team: Jose Sanchez, Knut Brunier, Anica Taneja, Diego Rossel
//Course Tutor: Alisa Andrasek

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

В рамках проекта в 2016 году были получены следующие результаты:

•   Разработан метод структурного анализа поведенческих свойств вложенных сетей Петри, основанный на эффективно вычислимых инвариантах позиций.
В рамках исследования предложено обобщение инвариантов позиций классических сетей Петри для моделей вложенных сетей Петри; предложен метод поиска инвариантов; показано, что инварианты позиций сохраняются во время исполнения модели. Данный метод позволяет доказывать свойства, важные для корректного поведения анализируемых систем. В частности, важное для реализуемости свойство ограниченности числа состояний фрагмента NP-сети следует из покрытия данного фрагмента инвариантами позиций.
На примере распределенной EJB системы, исследована и продемонстрирована применимость метода для доказательства свойств распределенных мультиагентных систем с мобильными агентами.

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

Ожидаемые результаты в 2017 году:

1) Метод композиционального анализа поведенческих свойств выраженных с помощью формул линейной темпоральной логики;
2) Разработка и реализация алгоритм проверки выполнимости формулы;
3) Аппробация разработанного метода на мультиагентной распределенной системе с мобильными агентами.