Modelling Dependable Systems with Modular Rewritable Stochastic Petri Nets

Petri Nets (PN) are commonly utilized as a robust formalism for concurrent systems; however, they face difficulties in effectively modeling adaptive systems. To mitigate this, "rewritable"PT nets (RwPT) have been recently developed using Maude, a declarative language that upholds rewriting logic semantics. A modular approach is proposed that employs algebraic operators to build extensive models and composite node labeling to maintain hierarchical structure through net rewrites. After incorporating stochastic parameters into the formalism, we present an automated process to derive a lumped CTMC from the quotient graph generated by a modular RwPT. We showcase the efficacy of our methodology using a gracefully degrading manufacturing system as a case study.