Résumé: Reconfigurable wireless ad hoc networks (R-WANETs) constitute a well-known paradigm of networks that change their structure to fulfill dynamic requirements and/or respond to their volatile environments. Several formalisms have been exploited and extended for the modeling, verification, and performance evaluation of R-WANETs. Distinguishably, generalized stochastic Petri nets (GSPNs) have been extended to some formalisms involved in the design of various kinds of networks. However, these extensions show many shortcomings. In particular, dynamic GSPNs (D-GSPNs) only allow the modeling and verification of reconfigurations in GSPNs under single-server semantics. This restriction was imposed to enable the transformation of D-GSPNs into basic GSPNs. In this paper, we extend D-GSPNs to a new formalism called improved D-GSPNs (ID-GSPNs), enabling the modeling and verification of dynamic nets whose transitions follow infinite-, single-, or multi-server semantics. Furthermore, a new algorithm that unfolds ID-GSPNs towards basic GSPNs while preserving their stochastic behaviors is provided. Additionally, the proposed algorithm yields more compact models than those obtained by existing unfolding algorithms. Finally, the proposed formalism is exploited in the modeling, verification, and performance evaluation of R-WANETs.

Langue: Anglais