Применение компонентных сетей Петри в задачах верификации параллельных распределенных систем - Научная работа

В работе рассмотрены модели Крипке двух математических моделей параллельных распределенных систем, представленных детальной и ее компонентной сетями Петри. Показана бисимулярность этих моделей Крипке. Установлены возможности проверки истинности логической формулы темпоральной логики, которой задается требуемое свойство исследуемой параллельной распределенной системы, с помощью редуцированной модели Крипке компонентной сети Петри. The paper discusses the Kripke structures of two mathematical models of parallel distributed systems that are presented by Petri detailed net and its component net.В этом направлении в работах [9, 10] предложено использование компонентной модели Петри (CN-сети), применение которой для моделирования систем с параллелизмом позволяет получать редуцированные CN-модели (модели значительно меньших размеров относительно исходной детальной модели N ). При этом имеют место бисимуляционная эквивалентность [11] компонентной сети Петри (CN-сети) исходной детальной модели Петри N исследуемой параллельной распределенной системы, эпимор-физм этих моделей [12] и их языков [13-15]. Алгоритмы верификации на модели с использованием логики ветвящегося времени (CTL - Computation Tree Logic) [17] являются эффективными инструментами анализа последовательностей состояний в исследуемых системах, объединяющими традиционные и логические методы анализа, где свойство системы задается в виде логической формулы, истинность которой проверяется на модели Крипке, представляющей поведение системы. 3) определено, каким образом устанавливать выполнимость формулой CTL логики на модели Крипке детальной модели Петри по выполнимости соответствующих формул CTL логики на модели Крипке компонентной модели Петри. Модель Крипке - это структура, отражающая достижимые в системе состояния, а это означает, что модель Крипке для сети Петри будет представляться графом достижимых в сети разметок.Компонентная сеть Петри, являясь адекватной редукцией детальных сетей Петри - выразительных математических моделей параллельных распределенных систем, обладающая значительно меньшими размерами, позволяет проводить эффективный анализ структурных свойств [10, 18], поведенческих свойств [13-15] исходной детальной сети Петри исследуемой параллельной распределенной системы. В работе проведены исследования на возможность применения компонентной сети Петри к верификации параллельных распределенных систем с использованием автоматической проверки с помощью метода Model Checking, предполагающего применение аппарата темпоральной логики CTL, проверка формул которой проводится на семантической модели Крипке. В работе показано, что проверку истинности логической формулы логики CTL, с помощью которой задается устанавливаемое свойство исследуемой параллельной распределенной системы, математическая модель которой представлена сетью Петри, можно проводить с помощью редуцированной модели Крипке ее компонентной сети Петри. Сети Петри. Design and synthesis of synchronization skeletons using branching time temporal logic // Lect.