Generalized Stochastic Petri Nets with Rewritable Topology

New developed software/hardware systems are open, dynamic, and flexible (as the case of reconfigurable wireless sensor networks, data centers, etc.). Often, the reliability is indispensable in these kinds of systems. Formal methods (as Petri nets (PNs)) are used to formally verify the reliability in critical systems. PNs are extended to generalized stochastic Petri nets (GSPNs) for the modeling and verification of stochastic systems. It is a popular formalism which is exploited in the analysis of various types of systems. Nevertheless, the rigid structure of GSPNs restricts their use in the study of reconfigurable systems and there may exist preliminary researches that tackle the reconfiguration in GSPNs. The aim of this work is to propose an extension to GSPNs called GSPNs with rewritable topology (GSPNs-RT) in order to provide a suitable tool for the formal modeling and verification of reconfigurable systems. The new GSPNs-RT formalism combines the GSPNs formalism, a set of transformation rules, and an algorithm used to transform a given GSPN-RT into an equivalent GSPN. This equivalent GSPN is used to apply classical verification methods proposed for GSPNs on GSPNs-RT. The feasibility of the new proposed formalism is demonstrated though a data center case study where both structural and behavioral analyses are carried out.