Efficient Performance Analysis of Modular Rewritable Petri Nets

TL;DR

This paper introduces a modular approach to modeling adaptive systems with Petri Nets using rewriting logic, enabling automated performance analysis through CTMC derivation, demonstrated on a manufacturing case study.

Contribution

It presents a novel modular framework for rewritable Petri Nets with hierarchical labeling and an automated method for performance analysis via CTMC derivation.

Findings

Effective modeling of adaptive systems using RwPT.

Automated derivation of CTMC from modular RwPT models.

Successful application to a fault-tolerant manufacturing system.

Abstract

Petri Nets (PN) are extensively used as a robust formalism to model concurrent and distributed systems; however, they encounter difficulties in accurately modeling adaptive systems. To address this issue, we defined rewritable PT nets (RwPT) using Maude, a declarative language that ensures consistent rewriting logic semantics. Recently, we proposed a modular approach that employs algebraic operators to build extensive RwPT models. This methodology uses composite node labeling to maintain hierarchical organization through net rewrites and has been shown to be effective. Once stochastic parameters are integrated into the formalism, we introduce an automated procedure to derive a lumped CTMC from the quotient graph generated by a modular RwPT model. To demonstrate the effectiveness of our method, we present a fault-tolerant manufacturing system as a case study.