Методы анализа моделей. Композиция кланов

Д.А. Зайцев, Цикл лекций "Моделирование сетями Петри и Слепцова" для научного лектория Ришельевского Лицея, Одесса, Лекция 2: "Методы анализа моделей. Композиция кланов", 2021, 30 слайдов, ссылка на видеозапись.На примере ранее построенных моделей сетевых протоколов изучаются основные методы анализа свойств сетей Петри. В качестве основной области применения выбрана верификация сетевых протоколов. Выполнен обзор других областей применения, таких как доказательство корректности параллельных и распределенных программ, автоматизация производства, организация бизнес-процессов, программирование контроллеров, управление движением транспорта и других. Анализ свойств сетей Петри выполнен методами теории графов в процессе построения графа достижимых (покрывающих) маркировок, а также методами линейной алгебры в процессе решения систем линейных диофантовых уравнений для нахождения инвариантов сети. Использована моделирующая система Tina Лаборатории архитектур систем, Тулуза, Франция. Представлены основы разработанной автором теории кланов линейных систем. Композиция кланов использована для ускорения решения больших систем в процессе верификации реальных протоколов. Изучены разновидности композиции кланов в процессе одновременного, последовательного и параллельно-последовательного коллапса графа декомпозиции системы. Выполнен обзор программного обеспечение Adriana и Deborah для декомпозиции системы на кланы и решения систем в процессе композиции кланов, реализованного в форме встраиваемых модулей системы Tina. Представлена новая совместная разработка с Лабораторией Инновационных Вычислений (Джека Донгарры), США - система ParAd (Parallel Adriana) для композиционного решения систем на современных параллельных и распределённых архитектурах.