Применение компонентных сетей Петри в задачах верификации параллельных распределённых систем

В работе рассмотрены модели Крипке двух математических моделей параллельных распределённых систем, представленных детальной и её компонентной сетями Петри. Показана бисимулярность этих моделей Крипке. Установлены возможности проверки истинности логической формулы темпоральной логики, которой задаётс...

Повний опис

Збережено в:

Бібліографічні деталі
Дата:	2014
Автор:	Лукьянова, Е.А.
Формат:	Стаття
Мова:	Russian
Опубліковано:	Інститут програмних систем НАН України 2014
Назва видання:	Проблеми програмування
Теми:	Паралельне програмування. Розподілені системи і мережі
Онлайн доступ:	http://dspace.nbuv.gov.ua/handle/123456789/113219
Теги:	Додати тег Немає тегів, Будьте першим, хто поставить тег для цього запису!
Назва журналу:	Digital Library of Periodicals of National Academy of Sciences of Ukraine
Цитувати:	Применение компонентных сетей Петри в задачах верификации параллельных распределённых систем / Е.А. Лукьянова // Проблеми програмування. — 2014. — № 2-3. — С. 93-98. — Бібліогр.: 19 назв. — рос.

Репозитарії

Digital Library of Periodicals of National Academy of Sciences of Ukraine

id	irk-123456789-113219
record_format	dspace
spelling	irk-123456789-1132192017-02-05T03:02:20Z Применение компонентных сетей Петри в задачах верификации параллельных распределённых систем Лукьянова, Е.А. Паралельне програмування. Розподілені системи і мережі В работе рассмотрены модели Крипке двух математических моделей параллельных распределённых систем, представленных детальной и её компонентной сетями Петри. Показана бисимулярность этих моделей Крипке. Установлены возможности проверки истинности логической формулы темпоральной логики, которой задаётся требуемое свойство исследуемой параллельной распределённой системы, с помощью редуцированной модели Крипке компонентной сети Петри. 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. Bisimularity of these Kripke structures is displayed. The possibility for checking the validity of the logical formula of temporal logic is established, which gives the desired property of investigated parallel distributed system, using reduced Kripke structure of component Petri net. 2014 Article Применение компонентных сетей Петри в задачах верификации параллельных распределённых систем / Е.А. Лукьянова // Проблеми програмування. — 2014. — № 2-3. — С. 93-98. — Бібліогр.: 19 назв. — рос. 1727-4907 http://dspace.nbuv.gov.ua/handle/123456789/113219 004.021: 004.312.4: 004.414.2 ru Проблеми програмування Інститут програмних систем НАН України
institution	Digital Library of Periodicals of National Academy of Sciences of Ukraine
collection	DSpace DC
language	Russian
topic	Паралельне програмування. Розподілені системи і мережі Паралельне програмування. Розподілені системи і мережі
spellingShingle	Паралельне програмування. Розподілені системи і мережі Паралельне програмування. Розподілені системи і мережі Лукьянова, Е.А. Применение компонентных сетей Петри в задачах верификации параллельных распределённых систем Проблеми програмування
description	В работе рассмотрены модели Крипке двух математических моделей параллельных распределённых систем, представленных детальной и её компонентной сетями Петри. Показана бисимулярность этих моделей Крипке. Установлены возможности проверки истинности логической формулы темпоральной логики, которой задаётся требуемое свойство исследуемой параллельной распределённой системы, с помощью редуцированной модели Крипке компонентной сети Петри.
format	Article
author	Лукьянова, Е.А.
author_facet	Лукьянова, Е.А.
author_sort	Лукьянова, Е.А.
title	Применение компонентных сетей Петри в задачах верификации параллельных распределённых систем
title_short	Применение компонентных сетей Петри в задачах верификации параллельных распределённых систем
title_full	Применение компонентных сетей Петри в задачах верификации параллельных распределённых систем
title_fullStr	Применение компонентных сетей Петри в задачах верификации параллельных распределённых систем
title_full_unstemmed	Применение компонентных сетей Петри в задачах верификации параллельных распределённых систем
title_sort	применение компонентных сетей петри в задачах верификации параллельных распределённых систем
publisher	Інститут програмних систем НАН України
publishDate	2014
topic_facet	Паралельне програмування. Розподілені системи і мережі
url	http://dspace.nbuv.gov.ua/handle/123456789/113219
citation_txt	Применение компонентных сетей Петри в задачах верификации параллельных распределённых систем / Е.А. Лукьянова // Проблеми програмування. — 2014. — № 2-3. — С. 93-98. — Бібліогр.: 19 назв. — рос.
series	Проблеми програмування
work_keys_str_mv	AT lukʹânovaea primeneniekomponentnyhsetejpetrivzadačahverifikaciiparallelʹnyhraspredelënnyhsistem
first_indexed	2025-07-08T05:23:23Z
last_indexed	2025-07-08T05:23:23Z
_version_	1837055035786133504
fulltext	Паралельне програмування. Розподілені системи і мережі © Е.А. Лукьянова, 2014 ISSN 1727-4907. Проблеми програмування. 2014. № 2–3. Спеціальний випуск 93 УДК 004.021: 004.312.4: 004.414.2 ПРИМЕНЕНИЕ КОМПОНЕНТНЫХ СЕТЕЙ ПЕТРИ В ЗАДАЧАХ ВЕРИФИКАЦИИ ПАРАЛЛЕЛЬНЫХ РАСПРЕДЕЛЁННЫХ СИСТЕМ Е.А. Лукьянова Таврический национальный университет имени В.И. Вернадского, факультет математики и информатики, проспект Вернадского, 4. E-mail: lukyanovaea@mail.ru В работе рассмотрены модели Крипке двух математических моделей параллельных распределённых систем, представленных д е- тальной и её компонентной сетями Петри. Показана бисимулярность этих моделей Крипке. Установлены возможности проверки истинности логической формулы темпоральной логики, которой задаётся требуемое свойство исследуемой параллельной распреде- лённой системы, с помощью редуцированной модели Крипке компонентной сети Петри. 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. Bisimularity of these Kripke structures is displayed. The possibility for checking the validity of the logical formula of temporal logic is established, which gives the desired property of investigated parallel distributed system, using reduced Kripke structure of component Petri net. Введение Параллельные распределённые системы представляют собой сложные вычислительные системы, в ко- торых выполняется параллельная обработка данных несколькими различными машинами системы, подклю- ченными к локальной или глобальной сети, при возможности, как синхронного, так и асинхронного управле- ния. Такие системы обладают недетерминированностью и характеризуются множеством взаимодействующих друг с другом процессов, результативно использующих все ресурсы сети. При этом сеть поддерживает функ- ционирование системы как единого целого, а каждая машина системы выполняет своё задание – часть функ- ций глобальной сети. Параллельные распределённые системы могут быть физическими, компьютерными или программными системами. В настоящее время дальнейшее перспективное развитие вычислительной техники на прямую связано с применением параллельных вычислительных систем, что в свою очередь обуславливает необходимость создания и использования новых или «модернизированных» моделей и методов параллель- ных вычислений и их реализаций, а так же разработки новых технологий проектирования параллельных рас- пределённых систем. При этом приходится решать задачи, связанные с согласованностью результатов моде- лирования с возможной дальнейшей верификацией и адекватностью полученных результатов для анализа соответствующих исследуемых свойств исходной изучаемой задачи. Теория параллельных систем и процессов имеет в своём арсенале достаточное количество разнообраз- ных моделей, алгоритмов и инструментов, которые могут быть использованы при моделировании, разработке и верификации параллельных распределенных систем. Применяются структурные [1–3] и семантические [4–6] формальные модели, позволяющие эффективно анализировать функциональные особенности, струк- турные и поведенческие свойства систем с параллелизмом. Используются алгебры [7, 8] и логики процессов, соответственно позволяющие представлять и изучать параллельные системы как элементы алгебры, разраба- тывать методы и способы спецификации и верификации параллельных процессов, используя различные ло- гические языки, например, аппараты логических языков темпоральных логик LTL, CTL, CTL. Изучаемые классы моделей характеризуются своей степенью выразительности и алгоритмической раз- решимости, а, значит, выбор используемого способа моделирования изучаемой системы имеет важное опре- деляющее значение. На сегодняшний день общепризнанно, что наилучшим формализмом, представляющим параллелизм в сложных реальных системах, является формализм сетей Петри. Применение современных мо- делей Петри, изучение их языков позволяет устанавливать как структурные, так и поведенческие свойства моделей, устанавливать взаимосвязи между моделями, используя различные поведенческие эквивалентности, например, применяя языковую, симуляционную, бисимуляционную эквивалентности. Это позволяет исполь- зовать высокую степень выразительности формализма сетей Петри с дальнейшими возможными преобразо- ваниями исходных моделей для получения адекватных моделей размеры, которых позволяли бы производить их продуктивный анализ. В этом направлении в работах [9, 10] предложено использование компонентной модели Петри (CN-сети), применение которой для моделирования систем с параллелизмом позволяет полу- чать редуцированные CN-модели (модели значительно меньших размеров относительно исходной детальной модели N ). При этом имеют место бисимуляционная эквивалентность [11] компонентной сети Петри (CN- сети) исходной детальной модели Петри N исследуемой параллельной распределённой системы, эпимор- физм этих моделей [12] и их языков [13–15]. mailto:lukyanovaea@mail.ru Паралельне програмування. Розподілені системи і мережі 94 1. Цель и задачи исследования В настоящей работе будут рассмотрены возможности использования, имеющихся результатов компонентного моделирования и инструментов компонентного анализа для верификации параллельных распределённых систем путём использования алгоритмического подхода, основанного на применении алгоритмов проверки на модели (model checking) [16]. Алгоритмы верификации на модели с использованием логики ветвящегося времени (CTL – Computation Tree Logic) [17] являются эффективными инструментами анализа последовательностей состояний в исследуемых системах, объединяющими традиционные и логические методы анализа, где свойство системы задается в виде логической формулы, истинность которой проверяется на модели Крипке, представляющей поведение системы. При этом необходимо уметь преодолевать проблему верификации реальных систем – анализ огромного числа состояний. Цель работы: установить, что отношение бисимуляции для детальной и компонентной моделей сохраняет выполнимость формул логики CTL, что позволит проводить проверку спецификации (формализованного в виде логической формулы проверяемого свойства исследуемой системы) на семантической модели Крипке редуци- рованной сети – CN-сети. Для этого в работе выполнены следующие шаги: 1) осуществлён переход от моделей Петри (двудольных графов) сетей N и CN к их соответствующим моделям Крипке (графам с одним типом вершин), на которых интерпретируется логика CTL; 2) выяснена бисимуляционная эквивалентность полученных моделей Крипке; 3) определено, каким образом устанавливать выполнимость формулой CTL логики на модели Крипке де- тальной модели Петри по выполнимости соответствующих формул CTL логики на модели Крипке компонент- ной модели Петри. Таким образом, основная задача – показать, что применение компонентной сети Петри, позволяющей выражать в достаточно компактном виде сложные системы с параллелизмом, может быть использовано и при верификации таких систем с использованием метода проверки на модели. 2. Модель Крипке для сетей Петри, моделирующих системы с параллельными процес- сами, с использованием компонентного моделирования Для исследуемой системы с параллельными процессами строится её формальная модель в виде деталь- ной сети Петри. Полученная сеть исследуется на наличие составных компонент [9, 18] (компонент-мест pC и компонент-переходов tC ). Результат – выделение в детальной модели Петри N составных компонент, в част- ности, наличие параллельных процессов обязательно обеспечит возможность выделения в детальной сети со- ставных компонент, при этом, в случае параллельных процессов, это могут быть либо одинаковые, либо одно- типные составные компоненты [19]. Таким образом, будет получена ещё одна формальная модель исходной исследуемой системы – компонентная сеть Петри CN, которая эпиморфна исходной детальной модели N [12]. Модель Крипке – это структура, отражающая достижимые в системе состояния, а это означает, что мо- дель Крипке для сети Петри будет представляться графом достижимых в сети разметок. Такая модель доста- точно выразительно представляет параллелизм – функционирование параллельных процессов (их поведение и взаимодействие). Имея две адекватные модели исследуемой системы (сети N и CN) построим для каждой её модель Крипке. Рассмотрим несколько примеров. На рис. 1, а показана небольшая сеть Петри, моделирующая функционирование двух синхронизируемых параллельных процессов, на рис. 1, б – её модель Крипке. а б Рис. 1. а – детальная сеть Петри, синхронизирующая два параллельных процесса; б – её модель Крипке Паралельне програмування. Розподілені системи і мережі 95 В рассматриваемой детальной сети Петри можно выделить одну составную компоненту – компоненту- переход, в которую практически полностью оформляются рассматриваемые два параллельных процесса и в которой происходит их синхронизация. На рис. 2, а, в соответственно показаны компонентная сеть Петри, отве- чающая исходной детальной сети Петри с рис. 1, а, и её модель Крипке. Эта компонентная сеть содержит со- ставную компоненту – компоненту-переход T , показанную на рис. 2, б. а б в Рис. 2. а – компонентная сеть Петри для сети Петри с рис. 1, а; б – её компонента-переход T ; в – её модель Крипке На рис. 3, а показана детальная сеть Петри из [15], синтезирующая два параллельных процесса. Данная сеть, хотя является и небольшой, её модель Крипке, отражающая достижимые состояния, для показа в работе достаточно громоздкая. Покажем её основной участок (рис. 3, б), который непосредственно и отражает син- тез независимо функционирующих параллельных процессов. Остальные состояния, не являющиеся суще- ственными характеристиками сети, из рассмотрения можно исключить в связи с тем, что рассматриваемые параллельные процессы функционируют самостоятельно (независимо друг от друга) и не синхронизируются, поэтому эти исключённые состояния являются «шумом» и только утяжеляют восприятие. а б Рис. 3. а – детальная сеть Петри, синтезирующая два параллельных процесса; б – участок её модели Крипке, отражающий синтез независимо функционирующих параллельных процессов В детальной сети Петри с рис. 3, а могут быть выделены составные компоненты несколькими варианта- ми, например, могут быть выделены три компоненты-места, две из которых будут одинаковыми, или могут быть выделены три одинаковые компоненты-переходы. Приведём вариант, когда в рассматриваемой детальной сети Петри будут выделены и компоненты-места и компоненты-переходы. Для этого варианта на рис. 4 а, д, соответственно показаны компонентная сеть Петри и её модель Крипке. Предложенная компонентная сеть со- держит одинаковые компоненты-переходы 1T , * 2T , показанные соответственно на рис. 4, б, в и компоненту- место P , показанную на рис. 4, г. Паралельне програмування. Розподілені системи і мережі 96 а б в г д Рис. 4. а – компонентная сеть Петри для сети Петри с рис. 3, а; б, в – её компоненты-переходы 1T и * 2T соответственно; г – её компонента-место P ; д – её модель Крипке В работе [11] установлена эквивалентность в функционировании детельной N и компонентной CN сетей Петри на уровне бисимуляционной эквивалентности. Бисимуляция сетей N и CN доказана на основании гомо- морфизма графов достижимых разметок сетей N и CN, обоснованного с помощью отношения компоненты 1 , введённого на множестве вершин графа достижимых разметок сети N . Установленная бисимуляция рассматри- валась как отношение, задаваемое на множестве вершин, объединения графов достижимых разметок, сетей N и CN. Учитывая вышесказанное и то, что модель Крипке для сети Петри представляется графом достижимых в сети разметок, получаем, что между вершинами моделей Крипке детальной и её компонентной сетей Петри имеется симметричное отношение R – бисимуляция, при котором для каждой пары Raa ),( 21 (где 1a и 2a – соответственно вершины моделей Крипке сети N и сети CN) выполняется следующее условие: если 11 'aa   (для некоторого действия  и вершины 1'a модели Крипке сети N ), то существует вер- шина 2'a модели Крипке сети CN, такая, что 2 2 'aa   и Raa )','( 21 . Действие  определяется из следующих знакосочетаний: 1) на множестве вершин некоторой модели Крипке определим знакосочетание 'aa   , где a , 'a – вер- шины модели Крипке,  – ребро из a в 'a ; 2) 2 1 aa   , когда либо 21 aa  , либо в модели Крипке есть путь из 1a в 2a с рёбрами, помеченными  ; 3) 2 * 1 aa   , когда либо   и 21 aa  , либо 2 * 2 1 * 1 '' aaaa   , где 1'a , 2'a некоторые вершины модели Крипке. Таким образом, модель Крипке компонентной сети CN бисимулярна модели Крипке соответствующей исходной детальной сети Петри N , значит, имеет место корректная редукция модели Крипке исходной детальной сети Петри исследуемой системы. Эта редукция заключается в том, что редуцированная модель Крипке имеет меньшее количество состояний и может быть получена как модель Крипке компонентной сети Петри исходной детальной сети Петри N , в которой предварительно выделяются составные компоненты (компоненты-места pC и компоненты-переходы tC ). 3. Модель Крипке компонентной сети Петри как модель её детальной сети Петри Формальная модель исследуемой системы представлена двумя её моделями: детальной сетью Петри N и её редуцированной компонентной сетью Петри CN. Построенные соответствующие для сетей N и CN модели Крипке обозначим соответственно NK и CNK . Модель Крипке выступает в качестве подробной схемы работы исследуемой системы, на которой можно выполнять проверку спецификаций системы, состоящих из набора формальных утверждений о свойствах, которым должна удовлетворять исследуемая система. Набор этих свойств будем задавать с помощью темпоральной логики – логики CTL. Формулы логики CTL строятся из элементарных высказываний, булевских функций и временных операторов. Используются временные операторы: («для всех путей вычисления»), («для некоторого пути вычисления»), между которыми выполняется отношение двойственности и за которыми следует один из следующих линейных временных операторов: («следующий момент»), («когда-то в будущем»), («всегда»), («до тех пор, пока»), («высвободить») [19]. Паралельне програмування. Розподілені системи і мережі 97 Модель Крипке NK представляется четвёркой ),,,( 0 fRGGKN  , где G – множество состояний, GG 0 – подмножество начальных состояний, GGR  – отношение переходов, )(: PBGf  – функция, помечающая каждое состояние множеством атомарных высказываний, истинных в этом состоянии, P – множество атомарных высказываний, )(PB – булеан множества P . Соответственно модель Крипке CNK – четвёрка )',',','( 0 fRGGKCN  . Отметим, что пути в моделях соответствуют вычислениям системы. И для модели Крипке ),,,( 0 fRGGK  , для каждого состояния Gg  и каждой формулы  CTL-логики ее значением )(g в состоянии g является булева константа 1 или 0, которая определяется индуктивно: 1) если Pp , то  определена в K ; 2) 0)0( ,1)1( defdef gg  ; 3) )()()( ),()()( ,)()(  gggggggg defdefdef  . Проверка набора формальных требований к функционированию системы на модели Крипке заключается в нахождении в множестве 0G подмножества всех состояний, в которых выполняется формула  и если этому подмножеству принадлежат все начальные состояния системы, то модель Крипке удовлетворяет свойству  . Множество состояний модели Крипке NK отношением компоненты 1 [11] разбивается на непересе- кающиеся классы эквивалентности, в каждый такой класс попадают состояния, для которых выполняются условия: 1) каждое состояние модели Крипке NK само с собой находится в отношении 1 ; 2) два состояния модели Крипке NK находятся в отношении 1 , если они являются состояниями одного участка модели Крипке NK , который отражает динамику функционирования соответствующей составной ком- поненты, выделенной в сети N . Если состояние модели Крипке NK не является состоянием ни одного из участков модели Крипке сети N , отражающего динамику функционирования составной компоненты, выделенной в N , то это состояние са- мо представляет класс эквивалентности – единичный класс. Отметим, что если при построении компонентной сети начальные вершины сети не включать в составные компоненты, то тогда начальные состояния моделей Крипке NK и CNK совпадают и при этом начальные состояния модели NK являются единичными классами эквивалентности. Согласно работе [11] рассмотренная бисимуляция моделей Крипке NK и CNK может быть определена через установление гомоморфизма h рассматриваемых моделей NK и CNK , в результате которого каждый уча- сток модели NK , отражающий динамику функционирования составной компоненты, инкапсулируется в одно состояние (состояние-инкапсулянт) в модели CNK , т.е. при отображении h каждый класс эквивалентности (единичный в том числе), построенный на множестве состояний модели NK по отношению 1 , отображается в соответствующее одно состояние модели CNK , что происходит с сохранением отношения переходов для обра- зов состояний модели NK . Имеют место следующие правила взаимосвязанной проверки для моделей NK и CNK : 1) для единичного класса эквивалентности и атомарного высказывания Pp выполняется ))((')( ghfgf  , где g – любое состояние из G , ')( ggh  , '' Gg  ; 2) для неединичного класса эквивалентности и атомарного высказывания Pp истинного в каждом состоянии участка модели Крипке NK , отражающего динамику функционирования соответствующей составной компоненты, выделенной в сети N , имеем истинность этого атомарного высказывания в соответствующем состоянии-инкапсулянте модели CNK ; 3) если атомарное высказывание Pp истинно в состоянии-инкапсулянте модели CNK , то проверку на истинность атомарного высказывания в модели NK достаточно проводить в состояниях только одного из одинаковых участков модели NK , отражающих динамику функционирования одинаковых составных компонент; Паралельне програмування. Розподілені системи і мережі 98 4) если формула  CTL-логики не выполняется на редуцированной модели Крипке CNK , то эта формула не выполняется и на модели Крипке исходной детальной модели Петри. Заключение Компонентная сеть Петри, являясь адекватной редукцией детальных сетей Петри – выразительных ма- тематических моделей параллельных распределённых систем, обладающая значительно меньшими размера- ми, позволяет проводить эффективный анализ структурных свойств [10, 18], поведенческих свойств [13–15] исходной детальной сети Петри исследуемой параллельной распределённой системы. В работе проведены исследования на возможность применения компонентной сети Петри к верификации параллельных распреде- лённых систем с использованием автоматической проверки с помощью метода Model Checking, предполага- ющего применение аппарата темпоральной логики CTL, проверка формул которой проводится на семантиче- ской модели Крипке. В работе показано, что проверку истинности логической формулы логики CTL, с помо- щью которой задаётся устанавливаемое свойство исследуемой параллельной распределённой системы, мате- матическая модель которой представлена сетью Петри, можно проводить с помощью редуцированной моде- ли Крипке её компонентной сети Петри. 1. Карп P.M., Миллер Р.Е. Параллельные схемы программ // Кибернетический сборник. – М.: Мир, 1976. – Т. 13. – С. 5–61. 2. Котов В.Е. Сети Петри. – М.: Наука, 1984. – 157 с. 3. Котов В.Е., Нариньяни А.С. Асинхронные вычислительные процессы над памятью // Кибернетика. – 1966. – № 3. – С. 64–71. 4. Clarke E.M., Emerson E.A. Design and synthesis of synchronization skeletons using branching time temporal logic // Lect. Notes Comput Sci. – 1981. – Vol. 131. – P. 52–71. 5. Jaffe J. The use of queues in parallel dataflow evaluation of 'if-then-while' programs // MIT, Laboratory for Computer Science. Tech. Rep. TM- 104, May 1978. 6. Roux J.-L., Berthomieu B. Verification of local area network protocol with Tine, a software package for time Petri nets // Proc. 7th Europ. Workshop on Application and Theory of Petri Nets. – 1986. – P. 183–205. 7. Zuberek W.M. Timed Petri nets and preliminary performance evaluation // Proc. 7th Annual Symp. on Сотр. Archit. – 1980. – P. 88–96. 8. Davis A.L. A data flow evaluation system based on the concept of recursive locality // Proc. Nat. Comput. Conf., New York, June 4 -7, 1979. Arlington: AFIPS Press. – 1979. – Vol. 48. – P. 1079–1086. 9. Лук’янова О.О. Про компонентне моделювання систем з паралелізмом // Наукові записки НаУКМА. Комп’ютерні науки. – 2012. – Т. 138. – C. 47–52. 10. Лукьянова Е.А. О компонентном анализе параллельных распределенных систем // ТВИМ. – 2011. – № 2. – С. 71–81. 11. Лук’янова О.О. Пробісимуляційну еквівалентність детальної моделі Петрі та її CN-моделі досліджуваної паралельної розподіленої системи // Вісник КНУ імені Тараса Шевченка. Серія: фізико-математичні науки. – 2013.– Спецвипуск. 12. Лукьянова Е.А. О гомоморфизме компонентной сети Петри // Кибернетика и системный анализ. – 2014. – № 1. 13. Лук’янова О.О. Про зв’язок мови CN-моделі з компонентами-переходам і мови детальної моделі Петрі паралельної розподіленої системи // Вісник КНУ імені Тараса Шевченка. Серія: фізико-математичні науки. – 2012. – № 4. – С. 145–150. 14. Lukyanova E. Component modeling: on connections of detailed Petri model and component model of parallel distributed system // ITHEA. – 2013. – Vol. 2, № 1. – P. 15–22. 15. Лукьянова Е.А. О языке компонентной сети Петри с компонентами-местами и компонентами-переходами // ТВИМ. – 2011. – № 2. – С. 71–81. 16. Clarke E.M., Grumberg O., Peled D. Model Checking // The MIT Press, 1999. – 314 p. 17. Kenneth L. McMillan Symbolic Model Checking. – CMU-CS-92-131. – 1992. 18. Лукьянова Е.А., Дереза А.В. Исследование однотипних структурних элементов CN-сети в процессе компонентного моделирования и анализа сложной системы с параллелизмом // Кибернетика и системный анализ. – 2012. – № 6. – С. 20–29. 19. Лукьянова Е.А. Метод верификации свойств реактивной системы на модели // ТВИМ. – 2006. – № 2. – C. 60–68.

Применение компонентных сетей Петри в задачах верификации параллельных распределённых систем

Репозитарії

Схожі ресурси