Глава
Layered Layouts for Software Systems Visualization Using Nested Petri Nets
В книге
Mногоуровневые мультиагентные системы (МАС) с динамической структурой широко используют- ся при решении важных прикладных задач в телекоммуникационных, транспортных, социальных и других системах. Поэтому обеспечение корректности таких систем является актуальной и значимой задачей. Одним из самых уязвимых для ошибок этапов разработки системы в рамках модельно- ориентированного подхода является этап реализации, на котором по разработанной модели строит- ся программный код. В данной работе представлен алгоритм автоматической трансляции моделей МАС в виде вложенных сетей Петри в системы распределенных компонентов. Вложенные сети Пет- ри являются расширением сетей Петри в рамках подхода “сети внутри сетей”, когда фишки в сети Петри сами могут являться сетями Петри, обладать автономным поведением и взаимодействовать с другими фишками сети. Это позволяет естественным образом моделировать МАС с динамической структурой. Представленная в работе трансляция сохраняет уровень распределенности и важные поведенче- ские свойства исходной модели (безопасность, живость, условная живость), а также обеспечивает справедливость исполнения целевой системы. Использование такой трансляции позволяет авто- матизировать построение распределенных МАС по моделям вложенных сетей Петри. В качестве апробации трансляция вложенных сетей Петри в распределенные системы компонентов была реа- лизована на основе компонентной технологии EJB.
Nested Petri nets (NP-nets) is an extension of Petri net formalism within the “nets-within-nets” approach, when tokens in a marking are Petri nets wich have autonomous behavior and synchronize with the system net. The formalism of NP-nets allows modeling multilevel multiagent systems with dynamic structure in a natural way. Currently there is no tool support for NP-nets simulation and analysis. The paper proposes translation of NP-nets into colored Petri nets and using CPN Tools as a virtual machine for NP-nets modeling, simulation and automatic verification.
Вложенные сети Петри (NP-nets) это сети Петри с сетевыми фишками. NP-nets являются расширением сетей Петри высокого уровня для моделирования активных объектов, мобильности и динамики в распределенных системах. В этой работе мы представляет алгоритм перевода двухуровневых NP-nets в поведенчески эквивалентную цветную сеть Петри, с целью применения методов и инструментов цветных сетей Петри для анализа NP-nets. Мы доказываем, что предложенная трансляция сохраняет динамическую семантику, с точностью до бисимуляционной эквивалентности.
Nested Petri nets (NP-nets) are Petri nets with net tokens. The liveness and boundedness problems are undecidable for two-level Nested Petri nets (NP-nets). Boundedness and liveness are still very hard to check even for plain Petri nets (EXPSPACE or worse). For the restricted class of free-choice Petri nets some problems become more amenable to analysis. There is the polynomial time algorithm to check if a free-choice Petri net is live and bounded. We prove that for some restricted class of NP-nets with free-choice components boundedness can be checked in a compositional way and define restrictions, under which liveness is also compositional. The motivating example of such restricted NP-nets is provided.
Nested Petri nets is an extension of Petri net formalism with net tokens for modelling multi-agent distributed systems with complex structure. Temporal logics, such as CTL, are used to state requirements of software systems behaviour. However, in the case of nested Petri nets models, CTL is not expressive enough for specification of system behaviour. In this paper we propose an extension of CTL with a new modality for specifying agents behavior. We define syntax and formal semantics for our logic, and give small examples of its usage.
Вложенные сети Петри являются одним из удобных формализмов для моделирования и анализа поведения распределенных мультиагентных систем. Они естественным образом представляют структуру мультиагентных систем, так как фишки в системной сети сами являются классическими сетями Петри и могут иметь автономное поведение. Мультиагентные системы являются системами с высоким уровнем параллелизма. При верификации таких систем методами проверки модели (model checking) возникают серьезные трудности, связанные с взрывным ростом числа промежуточных состояний системы (state-space explosion problem). Для решения этой проблемы в литературе был предложен подход, основанный на построении развертки поведения системы. Ранее была изучена применимость разверток для верификации вложенных сетей Петри и предложен метод построения разверток для безопасных консервативных вложенных сетей Петри. В этой работе предлагается другой метод построения разверток для безопасных консервативных вложенных сетей Петри, основанный на трансляции таких сетей в классические сети Петри. Для классических сетей Петри затем применяются стандартные методы построения разверток. Также в работе обсуждаются сравнительные достоинства двух подходов.